Termops API using EConstr.

3 files changed, 16 insertions, 13 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index b34a36492..79f185d18 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -79,13 +79,13 @@ type kind_of_formula=
 let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
-    match match_with_imp_term cciterm with
-	Some (a,b)-> Arrow(a,(pop b))
+    match match_with_imp_term (project gl) cciterm with
+	Some (a,b)-> Arrow(a,(pop (EConstr.of_constr b)))
       |_->
-	 match match_with_forall_term cciterm with
+	 match match_with_forall_term (project gl) cciterm with
 	     Some (_,a,b)-> Forall(a,b)
 	   |_->
-	      match match_with_nodep_ind cciterm with
+	      match match_with_nodep_ind (project gl) cciterm with
 		  Some (i,l,n)->
 		    let ind,u=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
@@ -96,7 +96,7 @@ let kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    Int.equal (nb_prod c) mib.mind_nparams in
+			    Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in
 			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
@@ -108,7 +108,7 @@ let kind_of_formula gl term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type cciterm with
+		    match match_with_sigma_type (project gl) cciterm with
 			Some (i,l)-> Exists((destInd i),l)
 		      |_-> Atom (normalize cciterm)
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 7ffc78928..1d107e9af 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,8 +38,8 @@ let wrap n b continue seq gls=
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env id) ctx then
+	    if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) ||
+	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
 	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index d9ab36ad6..01c019744 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -21,7 +21,10 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
+let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *)
+
 let unif t1 t2=
+  let evd = Evd.empty in (** FIXME *)
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -47,18 +50,18 @@ let unif t1 t2=
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Int.Set.is_empty (free_rels t) &&
-		  not (occur_term (mkMeta i) t) then
+		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Int.Set.is_empty (free_rels t) &&
-		  not (occur_term (mkMeta i) t) then
+		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
+	      Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;