diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-08 15:15:47 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-08 15:15:47 +0000 |
| commit | c4dccc430e10b784e65b5bf3330c55d658d2883d (patch) | |
| tree | 42afd0f7ff5f3c2079f65597fe15f46a1b830203 /library/declare.ml | |
| parent | b3e6d156fbc13ae6d79075265fc20f8912c520da (diff) | |
deplacement de Discharge dans toplevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/library/declare.ml b/library/declare.ml index c756d6169..b0ec97632 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -101,7 +101,7 @@ let declare_parameter id c = (* Constants. *) -type constant_declaration = constant_entry * strength * bool +type constant_declaration = constant_entry * strength let csttab = ref (Spmap.empty : constant_declaration Spmap.t) @@ -110,13 +110,13 @@ let _ = Summary.declare_summary "CONSTANT" Summary.unfreeze_function = (fun ft -> vartab := ft); Summary.init_function = (fun () -> vartab := Spmap.empty) } -let cache_constant (sp,((ce,_,_) as cd)) = +let cache_constant (sp,((ce,_) as cd)) = Global.add_constant sp ce; Nametab.push (basename sp) sp; declare_constant_implicits sp; csttab := Spmap.add sp cd !csttab -let load_constant (sp,((ce,_,_) as cd)) = +let load_constant (sp,((ce,_) as cd)) = declare_constant_implicits sp; csttab := Spmap.add sp cd !csttab @@ -184,7 +184,7 @@ let is_constant sp = try let _ = Global.lookup_constant sp in true with Not_found -> false let constant_strength sp = - let (_,stre,_) = Spmap.find sp !csttab in stre + let (_,stre) = Spmap.find sp !csttab in stre let is_variable id = let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab @@ -294,8 +294,7 @@ let declare_eliminations sp i = let mindstr = string_of_id (mis_typename mispec) in let declare na c = declare_constant (id_of_string na) - ({ const_entry_body = c; const_entry_type = None }, - NeverDischarge, false); + ({ const_entry_body = c; const_entry_type = None }, NeverDischarge); pPNL [< 'sTR na; 'sTR " is defined" >] in let env = Global.env () in |