diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 7 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 3 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 37 |
4 files changed, 40 insertions, 11 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 47f593ff3e..ffd8b71e5d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac = Pretyping.use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -344,7 +345,9 @@ let constr_flags () = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.fail_evar = false; - Pretyping.expand_evars = true } + Pretyping.expand_evars = true; + Pretyping.program_mode = false; +} let refine_tac ist simple with_classes c = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 7be8f67616..663537f3e8 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -56,7 +56,8 @@ let eval_uconstrs ist cs = Pretyping.use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } in let map c env sigma = c env sigma in List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2055b25ff4..7da4464e59 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1889,7 +1889,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = @@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 31e6b4c28f..30f716d764 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -542,7 +542,15 @@ let interp_gen kind ist pattern_mode flags env sigma c = invariant that running the tactic returned by push_trace does not modify sigma. *) let (_, dummy_proofview) = Proofview.init sigma [] in - let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in + + (* Again this is called at times with no open proof! *) + let name, poly = + try + let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + name, poly + with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false + in + let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term in @@ -556,7 +564,9 @@ let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; fail_evar = true; - expand_evars = true } + expand_evars = true; + program_mode = false; +} (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = @@ -570,19 +580,25 @@ let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; +} let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; +} let pure_open_constr_flags = { use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = false } + expand_evars = false; + program_mode = false; +} (* Interprets an open constr *) let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c = @@ -2045,7 +2061,16 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let name, poly = Id.of_string "ltac_sub", false in + (* XXX: This depends on the global state which is bad; the hooking + mechanism should be modified. *) + let name, poly = + try + let (_, poly, _) = Proof_global.get_current_persistence () in + let name = Proof_global.get_current_proof_name () in + name, poly + with | Proof_global.NoCurrentProof -> + Id.of_string "ltac_gen", false + in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in |