diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /library/dischargedhypsmap.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'library/dischargedhypsmap.mli')
| -rw-r--r-- | library/dischargedhypsmap.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 9a3259ce..f9d0f9b4 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dischargedhypsmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Libnames @@ -15,10 +15,10 @@ open Environ open Nametab (*i*) -type discharged_hyps = section_path list +type discharged_hyps = full_path list (*s Discharged hypothesis. Here we store the discharged hypothesis of each *) (* constant or inductive type declaration. *) -val set_discharged_hyps : section_path -> discharged_hyps -> unit -val get_discharged_hyps : section_path -> discharged_hyps +val set_discharged_hyps : full_path -> discharged_hyps -> unit +val get_discharged_hyps : full_path -> discharged_hyps |