diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 13:49:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 13:49:34 +0000 |
| commit | 242f8d2e8afb7da4302c07c2f1f8148bfa362b85 (patch) | |
| tree | 51c27923ba2bd9994eb49c1b3c22edceae154d27 /toplevel/command.ml | |
| parent | a37f10bd63aaabfb42867c371a720909b3d0c357 (diff) | |
Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le «load» des Remark/Fact
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index f53f26b8d..f290d684b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -75,7 +75,7 @@ let definition_body_red red_option ident (local,n) com comtypeopt = let ce' = red_constant_entry ce red_option in match n with | NeverDischarge -> declare_global_definition ident ce' n local - | DischargeAt disch_sp -> + | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let c = constr_of_constr_entry ce' in let sp = declare_variable ident (SectionLocalDef c,n,false) in @@ -115,7 +115,7 @@ let declare_global_assumption ident c = let hypothesis_def_var is_refining ident n c = match n with | NeverDischarge -> declare_global_assumption ident c - | DischargeAt disch_sp -> + | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let t = interp_type Evd.empty (Global.env()) c in let sp = declare_variable ident (SectionLocalAssum t,n,false) in @@ -437,7 +437,7 @@ let apply_tac_not_declare id pft = function let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const) strength = begin match strength with - | DischargeAt disch_sp when Lib.is_section_p disch_sp && not opacity -> + | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity -> let c = constr_of_constr_entry const in let _ = declare_variable id (SectionLocalDef c,strength,opacity) in () | NeverDischarge | DischargeAt _ -> |