Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

21 lines (16 sloc) 0.889 kb
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Libnames
open Term
open Environ
open Nametab
type discharged_hyps = full_path list
(** Discharged hypothesis. Here we store the discharged hypothesis of each
constant or inductive type declaration. *)
val set_discharged_hyps : full_path -> discharged_hyps -> unit
val get_discharged_hyps : full_path -> discharged_hyps
Jump to Line
Something went wrong with that request. Please try again.