From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 tactics/inv.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'tactics/inv.ml')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index e7d8249e4..d1d6178da 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -32,8 +32,9 @@ module NamedDecl = Context.Named.Declaration
 
 let var_occurs_in_pf gl id =
   let env = Proofview.Goal.env gl in
-  occur_var env id (Proofview.Goal.concl gl) ||
-  List.exists (occur_var_in_decl env id) (Proofview.Goal.hyps gl)
+  let sigma = project gl in
+  occur_var env sigma id (EConstr.of_constr (Proofview.Goal.concl gl)) ||
+  List.exists (occur_var_in_decl env sigma id) (Proofview.Goal.hyps gl)
 
 (* [make_inv_predicate (ity,args) C]
 
@@ -75,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	  let hyps_arity,_ = get_arity env indf in
 	    (hyps_arity,concl)
       | Dep dflt_concl ->
-	  if not (occur_var env id concl) then
+	  if not (occur_var env !evd id (EConstr.of_constr concl)) then
 	    user_err ~hdr:"make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id ++ str".");
           (* We abstract the conclusion of goal with respect to
@@ -183,7 +184,7 @@ let dependent_hyps env id idlist gl =
     | d::l ->
 	(* Update the type of id1: it may have been subject to rewriting *)
 	let d = pf_get_hyp (NamedDecl.get_id d) gl in
-	if occur_var_in_decl env id d
+	if occur_var_in_decl env (project gl) id d
         then d :: dep_rec l
         else dep_rec l
   in
@@ -448,7 +449,7 @@ let raw_inversion inv_kind id status names =
       make_inv_predicate env evdref indf realargs id status concl in
     let sigma = !evdref in
     let (cut_concl,case_tac) =
-      if status != NoDep && (dependent c concl) then
+      if status != NoDep && (dependent sigma (EConstr.of_constr c) (EConstr.of_constr concl)) then
         Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
         case_then_using
       else
@@ -514,12 +515,14 @@ let invIn k names ids id =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let concl = Proofview.Goal.concl gl in
-    let nb_prod_init = nb_prod concl in
+    let sigma = project gl in
+    let nb_prod_init = nb_prod sigma (EConstr.of_constr concl) in
     let intros_replace_ids =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_nf_concl gl in
+        let sigma = project gl in
         let nb_of_new_hyp =
-          nb_prod concl - (List.length hyps + nb_prod_init)
+          nb_prod sigma (EConstr.of_constr concl) - (List.length hyps + nb_prod_init)
         in
         if nb_of_new_hyp < 1 then
           intros_replacing ids
-- 
cgit v1.2.3