diff options
| author | Pierre-Marie Pédrot | 2016-11-18 20:35:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:53 +0100 |
| commit | 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 (patch) | |
| tree | f1ef11f826c498a78c9af6ffd9020fbc454dcd5e /tactics/autorewrite.ml | |
| parent | 8b660087beb2209e52bc4412dc82c6727963c6a5 (diff) | |
Equality API using EConstr.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index b567344c99..d656206d65 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -122,7 +122,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = Tacticals.New.tclTHEN tac (one_base (fun dir c tac -> let tac = (tac, conds) in - general_rewrite dir AllOccurrences true false ~tac c) + general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c)) tac_main bas)) (Proofview.tclUNIT()) lbas)) @@ -165,7 +165,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = | _ -> assert false) (* there must be at least an hypothesis *) | _ -> assert false (* rewriting cannot complete a proof *) in - let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in + let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in Tacticals.New.tclMAP (fun id -> Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> |