diff options
| author | msozeau | 2009-09-14 16:57:14 +0000 |
|---|---|---|
| committer | msozeau | 2009-09-14 16:57:14 +0000 |
| commit | a3645985be17e9fa8a8a5c4221aea40e189682c2 (patch) | |
| tree | 8f7f99638e715861976c69bb4df0b9bdeda120e2 /toplevel/command.ml | |
| parent | a764cfdbdfaecaa02f2fff0234fe1a198e0e34b5 (diff) | |
Backtrack on the forced discharge of type class variables introduced
by Context. Now Context has exactly the same semantics as Variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 80de344586..1da86712d1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -169,12 +169,12 @@ let syntax_definition ident (vars,c) local onlyparse = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = +let declare_one_assumption is_coe (local,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = declare_variable ident - (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in + (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ @@ -196,13 +196,13 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let declare_assumption_hook = ref ignore let set_declare_assumption_hook = (:=) declare_assumption_hook -let declare_assumption idl is_coe k bl c impl keep nl = +let declare_assumption idl is_coe k bl c impl nl = if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in let env = Global.env () in let c', imps = interp_type_evars_impls env c in !declare_assumption_hook c'; - List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl + List.iter (declare_one_assumption is_coe k c' imps impl nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -1106,7 +1106,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = | Local -> let impl=false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl,[]) in + let c = SectionLocalAssum (t_i,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Local,VarRef id,imps) | Global -> |