diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-18 20:35:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:53 +0100 |
| commit | 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 (patch) | |
| tree | f1ef11f826c498a78c9af6ffd9020fbc454dcd5e /plugins/funind/invfun.ml | |
| parent | 8b660087beb2209e52bc4412dc82c6727963c6a5 (diff) | |
Equality API using EConstr.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 36fb6dad3..d29d4694f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -385,7 +385,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* introducing the the result of the graph and the equality hypothesis *) observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); (* replacing [res] with its value *) - observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); + observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres))); (* Conclusion *) observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g) @@ -520,7 +520,7 @@ and intros_with_rewrite_aux : tactic = let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); generalize_dependent_of (destVar args.(1)) id; - tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id))); intros_with_rewrite ] g @@ -529,7 +529,7 @@ and intros_with_rewrite_aux : tactic = let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); generalize_dependent_of (destVar args.(2)) id; - tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id))); intros_with_rewrite ] g @@ -538,7 +538,7 @@ and intros_with_rewrite_aux : tactic = let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ[ Proofview.V82.of_tactic (Simple.intro id); - tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id))); intros_with_rewrite ] g end @@ -709,7 +709,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = in tclTHENSEQ[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; - Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); + Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma))); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) Proofview.V82.of_tactic (reduce |