diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 24 |
3 files changed, 17 insertions, 17 deletions
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 155cb31d85..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 @@ -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 *) |