diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:35:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:35:12 +0200 |
| commit | 8aa7de4ea2660fe370cedab07c1c5dcc19226c8c (patch) | |
| tree | 0eb6a177c3a14d50173183b0188b5f15b6c425c5 /tactics/eauto.ml | |
| parent | 75d70664156bf1715b4eb9933a684a344f43467d (diff) | |
| parent | 7ba6bc4554a642f78f59b996f99d9d6ca2cc2678 (diff) | |
Merge PR #805: Functional tactics
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 65864bd47..2b5bbfcd1 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -86,16 +86,16 @@ let rec prolog l n gl = let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl -let out_term = function +let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> let map c = let (sigma, c) = c (pf_env gl) (project gl) in let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in - out_term c + out_term (pf_env gl) c in let l = List.map map l in try (prolog l n gl) |