diff options
| author | gareuselesinge | 2013-08-08 18:52:52 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-08 18:52:52 +0000 |
| commit | c81254903e1e50a2305cd48ccfb673d9737afc48 (patch) | |
| tree | 622d6167cb84e4232794145801ab5ca87bde25fa /tactics | |
| parent | 80aba8d52c650ef8e4ada694c20bf12c15849694 (diff) | |
get rid of closures in global/proof state
In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/tactic_option.ml | 8 |
3 files changed, 7 insertions, 6 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index c855486db4..7a135bef06 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1825,12 +1825,12 @@ let add_morphism_infer glob m n = Flags.silently (fun () -> Lemmas.start_proof instance_id kind instance - (fun _ -> function + (Some (fun _ -> function Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) - | _ -> assert false); + | _ -> assert false)); Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) () let add_morphism glob binders m s n = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d8e03265d5..71312259ed 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1969,6 +1969,7 @@ let interp_tac_gen lfun avoid_ids debug t gl = gsigma = project gl; genv = pf_env gl } t) gl let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t +let _ = Proof_global.set_interp_tac interp let eval_ltac_constr gl t = interp_ltac_constr (default_ist ()) gl diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index fdd5a9aaed..9acf26f62e 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -14,13 +14,13 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = let default_tactic_expr : Tacexpr.glob_tactic_expr ref = Summary.ref default ~name:(name^"-default-tacexpr") in - let default_tactic : Proof_type.tactic ref = - Summary.ref (Tacinterp.eval_tactic !default_tactic_expr) ~name:(name^"-default-tactic") + let default_tactic : Tacexpr.glob_tactic_expr ref = + Summary.ref !default_tactic_expr ~name:(name^"-default-tactic") in let set_default_tactic local t = locality := local; default_tactic_expr := t; - default_tactic := Tacinterp.eval_tactic t + default_tactic := t in let cache (_, (local, tac)) = set_default_tactic local tac in let load (_, (local, tac)) = @@ -43,7 +43,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = set_default_tactic local tac; Lib.add_anonymous_leaf (input (local, tac)) in - let get () = !locality, !default_tactic in + let get () = !locality, Tacinterp.eval_tactic !default_tactic in let print () = Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++ (if !locality then str" (locally defined)" else str" (globally defined)") |