diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 730 |
1 files changed, 467 insertions, 263 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6fd95f16..f3482c31 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -1,26 +1,29 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp -open Pcoq open Genarg open Extraargs open Mod_subst open Names open Tacexpr -open Glob_term +open Glob_ops open Tactics +open Errors open Util open Evd open Equality -open Compat +open Misctypes +open Proofview.Notations + +DECLARE PLUGIN "extratactics" (**********************************************************************) (* admit, replace, discriminate, injection, simplify_eq *) @@ -30,76 +33,46 @@ TACTIC EXTEND admit [ "admit" ] -> [ admit_as_an_axiom ] END - - -let classes_dirpath = - make_dirpath (List.map id_of_string ["Classes";"Coq"]) - -let init_setoid () = - if Libnames.is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () - else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] - - -let occurrences_of occs = - let loccs = match occs with - | n::_ as nl when n < 0 -> (false,List.map (fun n -> ArgArg (abs n)) nl) - | nl -> - if List.exists (fun n -> n < 0) nl then - error "Illegal negative occurrence number."; - (true, List.map (fun n -> (ArgArg n)) nl) - in - init_setoid (); - {onhyps = Some []; concl_occs =loccs} - -let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = - Refiner.tclWITHHOLES false +let replace_in_clause_maybe_by (sigma,c1) c2 cl tac = + Proofview.Unsafe.tclEVARS sigma <*> (replace_in_clause_maybe_by c1 c2 cl) - sigma1 (Option.map Tacinterp.eval_tactic tac) -let replace_multi_term dir_opt (sigma,c) in_hyp = - Refiner.tclWITHHOLES false - (replace_multi_term dir_opt c) - sigma - (glob_in_arg_hyp_to_clause in_hyp) +let replace_term dir_opt (sigma,c) cl = + Proofview.Unsafe.tclEVARS sigma <*> + (replace_term dir_opt c) cl TACTIC EXTEND replace - ["replace" open_constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) tac ] -END - -TACTIC EXTEND replace_at - ["replace" open_constr(c1) "with" constr(c2) "at" occurrences(occs) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 (occurrences_of occs) tac ] + ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] +-> [ replace_in_clause_maybe_by c1 c2 cl tac ] END - TACTIC EXTEND replace_term_left - [ "replace" "->" open_constr(c) in_arg_hyp(in_hyp) ] - -> [ replace_multi_term (Some true) c in_hyp] + [ "replace" "->" open_constr(c) clause(cl) ] + -> [ replace_term (Some true) c cl ] END TACTIC EXTEND replace_term_right - [ "replace" "<-" open_constr(c) in_arg_hyp(in_hyp) ] - -> [replace_multi_term (Some false) c in_hyp] + [ "replace" "<-" open_constr(c) clause(cl) ] + -> [ replace_term (Some false) c cl ] END TACTIC EXTEND replace_term - [ "replace" open_constr(c) in_arg_hyp(in_hyp) ] - -> [ replace_multi_term None c in_hyp ] + [ "replace" open_constr(c) clause(cl) ] + -> [ replace_term None c cl ] END let induction_arg_of_quantified_hyp = function - | AnonHyp n -> ElimOnAnonHyp n - | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id) + | AnonHyp n -> None,ElimOnAnonHyp n + | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a ElimOnIdent and not as "constr" *) let elimOnConstrWithHoles tac with_evars c = - Refiner.tclWITHHOLES with_evars (tac with_evars) - c.sigma (Some (ElimOnConstr c.it)) + Tacticals.New.tclWITHHOLES with_evars (tac with_evars) + c.sigma (Some (None,ElimOnConstr c.it)) TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> @@ -120,9 +93,11 @@ TACTIC EXTEND esimplify_eq [ dEq true (Some (induction_arg_of_quantified_hyp h)) ] END +let discr_main c = elimOnConstrWithHoles discr_tac false c + TACTIC EXTEND discriminate_main | [ "discriminate" constr_with_bindings(c) ] -> - [ elimOnConstrWithHoles discr_tac false c ] + [ discr_main c ] END TACTIC EXTEND discriminate | [ "discriminate" ] -> [ discr_tac false None ] @@ -139,49 +114,55 @@ TACTIC EXTEND ediscriminate [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_discrHyp id gl = - h_discriminate_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl +open Proofview.Notations +let discrHyp id = + Proofview.tclEVARMAP >>= fun sigma -> + discr_main {it = Term.mkVar id,NoBindings; sigma = sigma;} + +let injection_main c = + elimOnConstrWithHoles (injClause None) false c TACTIC EXTEND injection_main | [ "injection" constr_with_bindings(c) ] -> - [ elimOnConstrWithHoles (injClause []) false c ] + [ injection_main c ] END TACTIC EXTEND injection -| [ "injection" ] -> [ injClause [] false None ] +| [ "injection" ] -> [ injClause None false None ] | [ "injection" quantified_hypothesis(h) ] -> - [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ] + [ injClause None false (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND einjection_main | [ "einjection" constr_with_bindings(c) ] -> - [ elimOnConstrWithHoles (injClause []) true c ] + [ elimOnConstrWithHoles (injClause None) true c ] END TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause [] true None ] -| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ] +| [ "einjection" ] -> [ injClause None true None ] +| [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND injection_as_main | [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ elimOnConstrWithHoles (injClause ipat) false c ] + [ elimOnConstrWithHoles (injClause (Some ipat)) false c ] END TACTIC EXTEND injection_as | [ "injection" "as" simple_intropattern_list(ipat)] -> - [ injClause ipat false None ] + [ injClause (Some ipat) false None ] | [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> - [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ] + [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ] END TACTIC EXTEND einjection_as_main | [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ elimOnConstrWithHoles (injClause ipat) true c ] + [ elimOnConstrWithHoles (injClause (Some ipat)) true c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" simple_intropattern_list(ipat)] -> - [ injClause ipat true None ] + [ injClause (Some ipat) true None ] | [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> - [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ] + [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_injHyp id gl = - h_injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl +let injHyp id = + Proofview.tclEVARMAP >>= fun sigma -> + injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; } TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] @@ -189,6 +170,10 @@ TACTIC EXTEND dependent_rewrite -> [ rewriteInHyp b c id ] END +(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to + "replace u with t" or "enough (t=u) as <-" and + "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) + TACTIC EXTEND cut_rewrite | [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ] | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] @@ -196,6 +181,17 @@ TACTIC EXTEND cut_rewrite END (**********************************************************************) +(* Decompose *) + +TACTIC EXTEND decompose_sum +| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ] +END + +TACTIC EXTEND decompose_record +| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ] +END + +(**********************************************************************) (* Contradiction *) open Contradiction @@ -206,7 +202,7 @@ END let onSomeWithHoles tac = function | None -> tac None - | Some c -> Refiner.tclWITHHOLES false tac c.sigma (Some c.it) + | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it) TACTIC EXTEND contradiction [ "contradiction" constr_with_bindings_opt(c) ] -> @@ -230,22 +226,19 @@ ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_stri END TACTIC EXTEND autorewrite -| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] -> - [ auto_multi_rewrite l (glob_in_arg_hyp_to_clause cl) ] -| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] -> +| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> + [ auto_multi_rewrite l ( cl) ] +| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> [ - let cl = glob_in_arg_hyp_to_clause cl in auto_multi_rewrite_with (Tacinterp.eval_tactic t) l cl - ] END TACTIC EXTEND autorewrite_star -| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) ] -> - [ auto_multi_rewrite ~conds:AllMatches l (glob_in_arg_hyp_to_clause cl) ] -| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] -> - [ let cl = glob_in_arg_hyp_to_clause cl in - auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ] +| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] -> + [ auto_multi_rewrite ~conds:AllMatches l cl ] +| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> + [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ] END (**********************************************************************) @@ -253,15 +246,8 @@ END let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in - Refiner. tclWITHHOLES false - (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true - -let occurrences_of = function - | n::_ as nl when n < 0 -> (false,List.map abs nl) - | nl -> - if List.exists (fun n -> n < 0) nl then - error "Illegal negative occurrence number."; - (true,nl) + Proofview.Unsafe.tclEVARS sigma <*> + general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> @@ -269,45 +255,62 @@ TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> [ rewrite_star (Some id) o (occurrences_of occ) c tac ] | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star (Some id) o Termops.all_occurrences c tac ] + [ rewrite_star (Some id) o Locus.AllOccurrences c tac ] | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> [ rewrite_star None o (occurrences_of occ) c tac ] | [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] -> - [ rewrite_star None o Termops.all_occurrences c tac ] + [ rewrite_star None o Locus.AllOccurrences c tac ] END (**********************************************************************) (* Hint Rewrite *) -let add_rewrite_hint name ort t lcsr = +let add_rewrite_hint bases ort t lcsr = let env = Global.env() and sigma = Evd.empty in - let f c = Topconstr.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in - add_rew_rules name (List.map f lcsr) - -VERNAC COMMAND EXTEND HintRewrite - [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] -> - [ add_rewrite_hint b o (Tacexpr.TacId []) l ] + let poly = Flags.is_universe_polymorphism () in + let f ce = + let c, ctx = Constrintern.interp_constr env sigma ce in + let ctx = + if poly then + Evd.evar_universe_context_set ctx + else + let cstrs = Evd.evar_universe_context_constraints ctx in + (Global.add_constraints cstrs; Univ.ContextSet.empty) + in + Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in + let eqs = List.map f lcsr in + let add_hints base = add_rew_rules base eqs in + List.iter add_hints bases + +let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater + +VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint + [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + [ add_rewrite_hint bl o None l ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) - ":" preident(b) ] -> - [ add_rewrite_hint b o t l ] + ":" preident_list(bl) ] -> + [ add_rewrite_hint bl o (Some t) l ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - [ add_rewrite_hint "core" o (Tacexpr.TacId []) l ] + [ add_rewrite_hint ["core"] o None l ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - [ add_rewrite_hint "core" o t l ] + [ add_rewrite_hint ["core"] o (Some t) l ] END (**********************************************************************) (* Hint Resolve *) open Term +open Vars open Coqlib -let project_hint pri l2r c = +let project_hint pri l2r r = + let gr = Smartlocate.global_with_alias r in let env = Global.env() in - let c = Constrintern.interp_constr Evd.empty env c in - let t = Retyping.get_type_of env Evd.empty c in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in let t = - Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in let sign,ccl = decompose_prod_assum t in let (a,b) = match snd (decompose_app ccl) with | [a;b] -> (a,b) @@ -317,82 +320,91 @@ let project_hint pri l2r c = let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in - (pri,true,Auto.PathAny,c) + let id = + Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) + in + let ctx = Evd.universe_context_set sigma in + let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in + (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = - Auto.add_hints true bl - (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc)) + Hints.add_hints true bl + (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIffLR - [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) +VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF + [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ add_hints_iff true lc n bl ] -| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] -> +| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> [ add_hints_iff true lc n ["core"] ] END -VERNAC COMMAND EXTEND HintResolveIffRL - [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) +VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF + [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ add_hints_iff false lc n bl ] -| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] -> +| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> [ add_hints_iff false lc n ["core"] ] END (**********************************************************************) (* Refine *) -open Refine +let refine_tac {Glob_term.closure=closure;term=term} = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let flags = Pretyping.all_no_fail_flags in + let tycon = Pretyping.OfType concl in + let lvar = { Pretyping.empty_lvar with + Pretyping.ltac_constrs = closure.Glob_term.typed; + Pretyping.ltac_uconstrs = closure.Glob_term.untyped; + Pretyping.ltac_idents = closure.Glob_term.idents; + } in + let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in + Tactics.New.refine ~unsafe:false update + end TACTIC EXTEND refine - [ "refine" casted_open_constr(c) ] -> [ refine c ] + [ "refine" uconstr(c) ] -> [ refine_tac c ] END -let refine_tac = h_refine - (**********************************************************************) (* Inversion lemmas (Leminv) *) open Inv open Leminv -VERNAC COMMAND EXTEND DeriveInversionClear - [ "Derive" "Inversion_clear" ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ] - -| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ] +let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater +VERNAC COMMAND EXTEND DeriveInversionClear | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (Glob_term.GProp Term.Null) false inv_clear_tac ] +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] + -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ] END open Term -open Glob_term VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_tac ] -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (GProp Null) false inv_tac ] - -| [ "Derive" "Inversion" ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ] - -| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ] +| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] + -> [ add_inversion_lemma_exn na c GProp false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_tac ] - END +END VERNAC COMMAND EXTEND DeriveDependentInversionClear | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] END @@ -401,14 +413,14 @@ END TACTIC EXTEND subst | [ "subst" ne_var_list(l) ] -> [ subst l ] -| [ "subst" ] -> [ fun gl -> subst_all gl ] +| [ "subst" ] -> [ subst_all () ] END let simple_subst_tactic_flags = { only_leibniz = true; rewrite_dependent_proof = false } TACTIC EXTEND simple_subst -| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags ] +| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags () ] END open Evar_tactics @@ -416,29 +428,28 @@ open Evar_tactics (**********************************************************************) (* Evar creation *) +(* TODO: add support for some test similar to g_constr.name_colon so that + expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END -open Tacexpr open Tacticals TACTIC EXTEND instantiate - [ "instantiate" "(" integer(i) ":=" glob(c) ")" hloc(hl) ] -> - [instantiate i c hl ] -| [ "instantiate" ] -> [ tclNORMEVAR ] + [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> + [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ] +| [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> + [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ] +| [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ] END - (**********************************************************************) (** Nijmegen "step" tactic for setoid rewriting *) open Tactics -open Tactics -open Libnames open Glob_term -open Summary open Libobject open Lib @@ -447,8 +458,8 @@ open Lib x R y -> x == z -> z R y (in the left table) *) -let transitivity_right_table = ref [] -let transitivity_left_table = ref [] +let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r" +let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" (* [step] tries to apply a rewriting lemma; then apply [tac] intended to complete to proof of the last hypothesis (assumed to state an equality) *) @@ -456,12 +467,12 @@ let transitivity_left_table = ref [] let step left x tac = let l = List.map (fun lem -> - tclTHENLAST - (apply_with_bindings (lem, ImplicitBindings [x])) + Tacticals.New.tclTHENLAST + (apply_with_bindings (lem, ImplicitBindings [x])) tac) !(if left then transitivity_left_table else transitivity_right_table) in - tclFIRST l + Tacticals.New.tclFIRST l (* Main function to push lemmas in persistent environment *) @@ -476,59 +487,43 @@ let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) let inTransitivity : bool * constr -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); + open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); subst_function = subst_transitivity_lemma; classify_function = (fun o -> Substitute o) } -(* Synchronisation with reset *) - -let freeze () = !transitivity_left_table, !transitivity_right_table - -let unfreeze (l,r) = - transitivity_left_table := l; - transitivity_right_table := r - -let init () = - transitivity_left_table := []; - transitivity_right_table := [] - -let _ = - declare_summary "transitivity-steps" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = init } - (* Main entry points *) let add_transitivity_lemma left lem = - let lem' = Constrintern.interp_constr Evd.empty (Global.env ()) lem in + let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) TACTIC EXTEND stepl | ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.eval_tactic tac) ] -| ["stepl" constr(c) ] -> [ step true c tclIDTAC ] +| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ] END TACTIC EXTEND stepr | ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.eval_tactic tac) ] -| ["stepr" constr(c) ] -> [ step false c tclIDTAC ] +| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ] END -VERNAC COMMAND EXTEND AddStepl +VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF | [ "Declare" "Left" "Step" constr(t) ] -> [ add_transitivity_lemma true t ] END -VERNAC COMMAND EXTEND AddStepr +VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF | [ "Declare" "Right" "Step" constr(t) ] -> [ add_transitivity_lemma false t ] END -VERNAC COMMAND EXTEND ImplicitTactic +VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF | [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] +| [ "Clear" "Implicit" "Tactic" ] -> + [ Pfedit.clear_implicit_tactic () ] END @@ -537,10 +532,10 @@ END (**********************************************************************) (*spiwack : Vernac commands for retroknowledge *) -VERNAC COMMAND EXTEND RetroknowledgeRegister +VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in - let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in + [ let tc,ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in + let tb,ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in Global.register f tc tb ] END @@ -567,7 +562,7 @@ END during dependent induction. For internal use. *) TACTIC EXTEND specialize_eqs -[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ] +[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ] END (**********************************************************************) @@ -579,26 +574,36 @@ END (**********************************************************************) let subst_var_with_hole occ tid t = - let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in + let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function | GVar (_,id) as x -> - if id = tid - then (decr occref; if !occref = 0 then x - else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) + if Id.equal id tid + then + (decr occref; + if Int.equal !occref 0 then x + else + (incr locref; + GHole (Loc.make_loc (!locref,0), + Evar_kinds.QuestionMark(Evar_kinds.Define true), + Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t in - if !occref > 0 then Termops.error_invalid_occurrence [occ] else t' + if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evd.QuestionMark(Evd.Define true)) -> - decr occref; if !occref = 0 then tc - else (incr locref; GHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> + decr occref; + if Int.equal !occref 0 then tc + else + (incr locref; + GHole (Loc.make_loc (!locref,0), + Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t @@ -606,31 +611,38 @@ let subst_hole_with_term occ tc t = open Tacmach let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x -let hResolve id c occ t gl = - let sigma = project gl in - let env = Termops.clear_named_body id (pf_env gl) in +let hResolve id c occ t = + Proofview.Goal.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Termops.clear_named_body id (Proofview.Goal.env gl) in + let concl = Proofview.Goal.concl gl in let env_ids = Termops.ids_of_context env in - let env_names = Termops.names_of_rel_context env in - let c_raw = Detyping.detype true env_ids env_names c in - let t_raw = Detyping.detype true env_ids env_names t in + let c_raw = Detyping.detype true env_ids env sigma c in + let t_raw = Detyping.detype true env_ids env sigma t in let rec resolve_hole t_hole = try - Pretyping.Default.understand sigma env t_hole - with - | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> - resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) + Pretyping.understand env sigma t_hole + with + | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> + let (e, info) = Errors.push e in + let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in + resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) in - let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in + let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in + let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in - change_in_concl None (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl)) gl + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) + end -let hResolve_auto id c t gl = +let hResolve_auto id c t = let rec resolve_auto n = try - hResolve id c n t gl + hResolve id c n t with | UserError _ as e -> raise e | e when Errors.noncritical e -> resolve_auto (n+1) @@ -646,18 +658,18 @@ END hget_evar *) -open Evar_refiner -open Sign - -let hget_evar n gl = - let sigma = project gl in - let evl = evar_list sigma (pf_concl gl) in +let hget_evar n = + Proofview.Goal.nf_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let evl = evar_list concl in if List.length evl < n then error "Not enough uninstantiated existential variables."; if n <= 0 then error "Incorrect existential variable index."; let ev = List.nth evl (n-1) in let ev_type = existential_type sigma ev in - change_in_concl None (mkLetIn (Anonymous,mkEvar ev,ev_type,pf_concl gl)) gl + change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) + end TACTIC EXTEND hget_evar | [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ] @@ -673,12 +685,15 @@ END (* Contributed by Julien Forest and Pierre Courtieu (july 2010) *) (**********************************************************************) -exception Found of tactic +exception Found of unit Proofview.tactic -let rewrite_except h g = - tclMAP (fun id -> if id = h then tclIDTAC else - tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true true id (mkVar h) false)) - (Tacmach.pf_ids_of_hyps g) g +let rewrite_except h = + Proofview.Goal.nf_enter begin fun gl -> + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else + Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) + hyps + end let refl_equal = @@ -691,31 +706,39 @@ let refl_equal = (* This is simply an implementation of the case_eq tactic. this code should be replaced by a call to the tactic but I don't know how to call it before it is defined. *) -let mkCaseEq a : tactic = - (fun g -> - let type_of_a = Tacmach.pf_type_of g a in - tclTHENLIST - [Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; - (fun g2 -> - change_in_concl None - (Tacred.pattern_occs [((false,[1]), a)] (Tacmach.pf_env g2) Evd.empty (Tacmach.pf_concl g2)) - g2); - simplest_case a] g);; - - -let case_eq_intros_rewrite x g = - let n = nb_prod (Tacmach.pf_concl g) in - Pp.msgnl (Printer.pr_lconstr x); - tclTHENLIST [ +let mkCaseEq a : unit Proofview.tactic = + Proofview.Goal.nf_enter begin fun gl -> + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in + Tacticals.New.tclTHENLIST + [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + change_concl + (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)) + end; + simplest_case a] + end + + +let case_eq_intros_rewrite x = + Proofview.Goal.nf_enter begin fun gl -> + let n = nb_prod (Proofview.Goal.concl gl) in + (* Pp.msgnl (Printer.pr_lconstr x); *) + Tacticals.New.tclTHENLIST [ mkCaseEq x; - (fun g -> - let n' = nb_prod (Tacmach.pf_concl g) in - let h = fresh_id (Tacmach.pf_ids_of_hyps g) (id_of_string "heq") g in - tclTHENLIST [ (tclDO (n'-n-1) intro); - Tacmach.introduction h; - rewrite_except h] g - ) - ] g + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let hyps = Tacmach.New.pf_ids_of_hyps gl in + let n' = nb_prod concl in + let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in + Tacticals.New.tclTHENLIST [ + Tacticals.New.tclDO (n'-n-1) intro; + introduction h; + rewrite_except h] + end + ] + end let rec find_a_destructable_match t = match kind_of_term t with @@ -724,40 +747,52 @@ let rec find_a_destructable_match t = (* TODO check there is no rel n. *) raise (Found (Tacinterp.eval_tactic(<:tactic<destruct x>>))) else - let _ = Pp.msgnl (Printer.pr_lconstr x) in + (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) raise (Found (case_eq_intros_rewrite x)) | _ -> iter_constr find_a_destructable_match t let destauto t = try find_a_destructable_match t; - error "No destructable match found" + Proofview.tclZERO (UserError ("", str"No destructable match found")) with Found tac -> tac -let destauto_in id g = - let ctype = Tacmach.pf_type_of g (mkVar id) in - Pp.msgnl (Printer.pr_lconstr (mkVar id)); - Pp.msgnl (Printer.pr_lconstr (ctype)); - destauto ctype g +let destauto_in id = + Proofview.Goal.nf_enter begin fun gl -> + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in +(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) +(* Pp.msgnl (Printer.pr_lconstr (ctype)); *) + destauto ctype + end TACTIC EXTEND destauto -| [ "destauto" ] -> [ (fun g -> destauto (Tacmach.pf_concl g) g) ] +| [ "destauto" ] -> [ Proofview.Goal.nf_enter (fun gl -> destauto (Proofview.Goal.concl gl)) ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END (* ********************************************************************* *) +let eq_constr x y = + Proofview.Goal.enter (fun gl -> + let evd = Proofview.Goal.sigma gl in + if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () + else Tacticals.New.tclFAIL 0 (str "Not equal")) + TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ - if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ] +| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] +END + +TACTIC EXTEND constr_eq_nounivs +| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [ + if eq_constr_nounivs x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] END TACTIC EXTEND is_evar | [ "is_evar" constr(x) ] -> [ match kind_of_term x with - | Evar _ -> tclIDTAC - | _ -> tclFAIL 0 (str "Not an evar") + | Evar _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") ] END @@ -776,28 +811,36 @@ let rec has_evar x = has_evar t1 || has_evar t2 || has_evar_array ts | Fix ((_, tr)) | CoFix ((_, tr)) -> has_evar_prec tr + | Proj (p, c) -> has_evar c and has_evar_array x = - array_exists has_evar x + Array.exists has_evar x and has_evar_prec (_, ts1, ts2) = - array_exists has_evar ts1 || array_exists has_evar ts2 + Array.exists has_evar ts1 || Array.exists has_evar ts2 TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> - [ if has_evar x then tclIDTAC else tclFAIL 0 (str "No evars") ] + [ if has_evar x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") ] END TACTIC EXTEND is_hyp | [ "is_var" constr(x) ] -> [ match kind_of_term x with - | Var _ -> tclIDTAC - | _ -> tclFAIL 0 (str "Not a variable or hypothesis") ] + | Var _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ] END TACTIC EXTEND is_fix | [ "is_fix" constr(x) ] -> [ match kind_of_term x with - | Fix _ -> Tacticals.tclIDTAC - | _ -> Tacticals.tclFAIL 0 (Pp.str "not a fix definition") ] + | Fix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] +END;; + +TACTIC EXTEND is_cofix +| [ "is_cofix" constr(x) ] -> + [ match kind_of_term x with + | CoFix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] END;; (* Command to grab the evars left unresolved at the end of a proof. *) @@ -805,8 +848,169 @@ END;; the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -[ "Grab" "Existential" "Variables" ] -> - [ let p = Proof_global.give_me_the_proof () in - Proof.V82.grab_evars p; - Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ] +[ "Grab" "Existential" "Variables" ] + => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] + -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] +END + +(* Shelves all the goals under focus. *) +TACTIC EXTEND shelve +| [ "shelve" ] -> + [ Proofview.shelve ] +END + +(* Shelves the unifiable goals under focus, i.e. the goals which + appear in other goals under focus (the unfocused goals are not + considered). *) +TACTIC EXTEND shelve_unifiable +| [ "shelve_unifiable" ] -> + [ Proofview.shelve_unifiable ] +END + +(* Command to add every unshelved variables to the focus *) +VERNAC COMMAND EXTEND Unshelve +[ "Unshelve" ] + => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] + -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ] +END + +(* Gives up on the goals under focus: the goals are considered solved, + but the proof cannot be closed until the user goes back and solve + these goals. *) +TACTIC EXTEND give_up +| [ "give_up" ] -> + [ Proofview.give_up ] +END + +(* cycles [n] goals *) +TACTIC EXTEND cycle +| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle (out_arg n) ] +END + +(* swaps goals number [i] and [j] *) +TACTIC EXTEND swap +| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap (out_arg i) (out_arg j) ] +END + +(* reverses the list of focused goals *) +TACTIC EXTEND revgoals +| [ "revgoals" ] -> [ Proofview.revgoals ] +END + + +type cmp = + | Eq + | Lt | Le + | Gt | Ge + +type 'i test = + | Test of cmp * 'i * 'i + +let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 None "cmp" +let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = + Genarg.make0 None "tactest" + +let pr_cmp = function + | Eq -> Pp.str"=" + | Lt -> Pp.str"<" + | Le -> Pp.str"<=" + | Gt -> Pp.str">" + | Ge -> Pp.str">=" + +let pr_cmp' _prc _prlc _prt = pr_cmp + +let pr_test_gen f (Test(c,x,y)) = + Pp.(f x ++ pr_cmp c ++ f y) + +let pr_test = pr_test_gen (Pptactic.pr_or_var Pp.int) + +let pr_test' _prc _prlc _prt = pr_test + +let pr_itest = pr_test_gen Pp.int + +let pr_itest' _prc _prlc _prt = pr_itest + + + +ARGUMENT EXTEND comparison TYPED AS cmp PRINTED BY pr_cmp' +| [ "=" ] -> [ Eq ] +| [ "<" ] -> [ Lt ] +| [ "<=" ] -> [ Le ] +| [ ">" ] -> [ Gt ] +| [ ">=" ] -> [ Ge ] + END + +let interp_test ist gls = function + | Test (c,x,y) -> + project gls , + Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y) + +ARGUMENT EXTEND test + PRINTED BY pr_itest' + INTERPRETED BY interp_test + RAW_TYPED AS test + RAW_PRINTED BY pr_test' + GLOB_TYPED AS test + GLOB_PRINTED BY pr_test' +| [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ] +END + +let interp_cmp = function + | Eq -> Int.equal + | Lt -> ((<):int->int->bool) + | Le -> ((<=):int->int->bool) + | Gt -> ((>):int->int->bool) + | Ge -> ((>=):int->int->bool) + +let run_test = function + | Test(c,x,y) -> interp_cmp c x y + +let guard tst = + if run_test tst then + Proofview.tclUNIT () + else + let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in + Proofview.tclZERO (Errors.UserError("guard",msg)) + + +TACTIC EXTEND guard +| [ "guard" test(tst) ] -> [ guard tst ] +END + +let decompose l c = + Proofview.Goal.enter begin fun gl -> + let to_ind c = + if isInd c then Univ.out_punivs (destInd c) + else error "not an inductive type" + in + let l = List.map to_ind l in + Elim.h_decompose l c + end + +TACTIC EXTEND decompose +| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] +END + +(** library/keys *) + +VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF +| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ + let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in + let k1 = Keys.constr_key (it c) in + let k2 = Keys.constr_key (it c') in + match k1, k2 with + | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 + | _ -> () ] +END + +VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY +| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ] +END + + +VERNAC COMMAND EXTEND OptimizeProof +| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] -> + [ Proof_global.compact_the_proof () ] +| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> + [ Gc.compact () ] END |