From 8cfe40dbc02156228a529c01190c50d825495013 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 22 Mar 2017 19:06:54 +0100 Subject: Ensuring static invariants about handling of pending evars in Pretyping. All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. --- plugins/ltac/tacinterp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 155cb31d85..6ed96c1fb7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1787,7 +1787,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) - ((sigma,sigma'),c) clp eqpat) sigma') + (sigma,c) clp eqpat) sigma') end } (* Derived basic tactics *) -- cgit v1.2.3 From f9526a2bcd05174b7adfe56b7375f0306a2a1e6d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Mar 2017 08:38:00 +0100 Subject: Fast path for implicit tactic solving. We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately. --- plugins/ltac/extratactics.ml4 | 8 ++++---- plugins/ltac/g_auto.ml4 | 2 +- plugins/ltac/tacinterp.ml | 22 +++++++++++----------- 3 files changed, 16 insertions(+), 16 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 1223f6eb4b..7a9fc6657e 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac = let flags = { Pretyping.use_typeclasses = false; solve_unification_constraints = true; - use_hook = Some Pfedit.solve_by_implicit_tactic; + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } in @@ -341,10 +341,10 @@ END (**********************************************************************) (* Refine *) -let constr_flags = { +let constr_flags () = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic; + Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = false; Pretyping.expand_evars = true } @@ -353,7 +353,7 @@ let refine_tac ist simple with_classes c = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = - { constr_flags with Pretyping.use_typeclasses = with_classes } in + { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index fcc2b86a91..f75ea70872 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -45,7 +45,7 @@ let eval_uconstrs ist cs = let flags = { Pretyping.use_typeclasses = false; solve_unification_constraints = true; - use_hook = Some Pfedit.solve_by_implicit_tactic; + use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6ed96c1fb7..fe10f0c313 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = Proofview.NonLogical.run (db_constr (curr_debug ist) env c); (evd,c) -let constr_flags = { +let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = Some solve_by_implicit_tactic; + use_hook = solve_by_implicit_tactic (); fail_evar = true; expand_evars = true } (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = - interp_gen kind ist false constr_flags env sigma c + interp_gen kind ist false (constr_flags ()) env sigma c let interp_constr = interp_constr_gen WithoutTypeConstraint let interp_type = interp_constr_gen IsType -let open_constr_use_classes_flags = { +let open_constr_use_classes_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = Some solve_by_implicit_tactic; + use_hook = solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } -let open_constr_no_classes_flags = { +let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = Some solve_by_implicit_tactic; + use_hook = solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } @@ -679,11 +679,11 @@ let pure_open_constr_flags = { expand_evars = false } (* Interprets an open constr *) -let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist = +let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c = let flags = - if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags - else open_constr_use_classes_flags in - interp_gen expected_type ist false flags + if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags () + else open_constr_use_classes_flags () in + interp_gen expected_type ist false flags env sigma c let interp_pure_open_constr ist = interp_gen WithoutTypeConstraint ist false pure_open_constr_flags -- cgit v1.2.3