Inv API using EConstr.

6 files changed, 34 insertions, 36 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 596f1a759..2d5c28eba 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -119,7 +119,6 @@ let contradiction_term (c,lbind as cl) =
     let typ = type_of c in
     let typ = EConstr.of_constr typ in
     let _, ccl = splay_prod env sigma typ in
-    let ccl = EConstr.of_constr ccl in
     if is_empty_type sigma ccl then
       Tacticals.New.tclTHEN
         (elim false None cl None)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6681e5e49..36ed589b9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -470,10 +470,11 @@ let match_eq_nf gls eqn (ref, hetero) =
   let n = if hetero then 4 else 3 in
   let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
   let pat = mkPattern (mkGAppRef ref args) in
+  let pf_whd_all gls c = EConstr.of_constr (pf_whd_all gls (EConstr.of_constr c)) in
   match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,pf_whd_all gls (EConstr.of_constr x),pf_whd_all gls (EConstr.of_constr y))
+	(EConstr.of_constr t,pf_whd_all gls x,pf_whd_all gls y)
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 094d62df6..c061c50f0 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -146,7 +146,7 @@ val is_matching_sigma : evar_map -> constr -> bool
 val match_eqdec : evar_map -> constr -> bool * Constr.constr * Constr.constr * Constr.constr * Constr.constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (Constr.constr * Constr.constr * Constr.constr)
+val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
 val is_matching_not : evar_map -> constr -> bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ad2e2fa3b..37c82ff64 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -12,8 +12,9 @@ open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
+open EConstr
+open Vars
 open Namegen
 open Environ
 open Inductiveops
@@ -62,10 +63,10 @@ let var_occurs_in_pf gl id =
 
  *)
 
-type inversion_status = Dep of constr option | NoDep
+type inversion_status = Dep of EConstr.constr option | NoDep
 
 let compute_eqn env sigma n i ai =
-  (mkRel (n-i),get_type_of env sigma (EConstr.of_constr (mkRel (n-i))))
+  (mkRel (n-i),EConstr.of_constr (get_type_of env sigma (mkRel (n-i))))
 
 let make_inv_predicate env evd indf realargs id status concl =
   let nrealargs = List.length realargs in
@@ -76,7 +77,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 !evd id (EConstr.of_constr concl)) then
+	  if not (occur_var env !evd id 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
@@ -86,13 +87,14 @@ let make_inv_predicate env evd indf realargs id status concl =
             match dflt_concl with
               | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
               | None ->
-		let sort = get_sort_family_of env !evd (EConstr.of_constr concl) in
+		let sort = get_sort_family_of env !evd concl in
 		let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
 		let p = make_arity env true indf sort in
+		let p = EConstr.of_constr p in
 		let evd',(p,ptyp) = Unification.abstract_list_all env
-                  !evd (EConstr.of_constr p) (EConstr.of_constr concl) (List.map EConstr.of_constr realargs@[EConstr.mkVar id])
-		in evd := evd'; EConstr.Unsafe.to_constr p in
-	  let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in
+                  !evd p concl (realargs@[mkVar id])
+		in evd := evd'; p in
+	  let hyps,bodypred = decompose_lam_n_assum !evd (nrealargs+1) pred in
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
   in
@@ -110,34 +112,28 @@ let make_inv_predicate env evd indf realargs id status concl =
         let ai = lift nhyps ai in
         let (xi, ti) = compute_eqn env' !evd nhyps n ai in
         let (lhs,eqnty,rhs) =
-          if closed0 ti then
+          if closed0 !evd ti then
 	    (xi,ti,ai)
           else
-            let xi = EConstr.of_constr xi in
-            let ti = EConstr.of_constr ti in
-            let ai = EConstr.of_constr ai in
 	    let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in
-	    let (xi, ti, ai) = res in
-            let xi = EConstr.Unsafe.to_constr xi in
-            let ti = EConstr.Unsafe.to_constr ti in
-            let ai = EConstr.Unsafe.to_constr ai in
-            let res = (xi, ti, ai) in
 	      evd := sigma; res
 	in
         let eq_term = eqdata.Coqlib.eq in
 	let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
+        let eq = EConstr.of_constr eq in
         let eqn = applist (eq,[eqnty;lhs;rhs]) in
         let eqns = (Anonymous, lift n eqn) :: eqns in
         let refl_term = eqdata.Coqlib.refl in
 	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
+	let refl_term = EConstr.of_constr refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
-	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr refl) in
+	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
         let args = refl :: args in
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
-  let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
-  let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr predicate) in
+  let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in
+  let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   predicate, args
@@ -347,10 +343,11 @@ let projectAndApply as_mode thin avoid id eqname names depids =
   in
   let substHypIfVariable tac id =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = project gl in
     (** We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
     let (t,t1,t2) = Hipattern.dest_nf_eq gl (EConstr.of_constr hyp) in
-    match (kind_of_term t1, kind_of_term t2) with
+    match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
     | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
     | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2
     | _ -> tac id
@@ -444,42 +441,42 @@ let raw_inversion inv_kind id status names =
     let sigma = Sigma.to_evar_map sigma in
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
+    let concl = EConstr.of_constr concl in
     let c = mkVar id in
     let (ind, t) =
-      try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c)))
+      try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c))
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
         CErrors.user_err  msg
     in
     let IndType (indf,realargs) = find_rectype env sigma t in
+    let realargs = List.map EConstr.of_constr realargs in
     let evdref = ref sigma in
     let (elim_predicate, args) =
       make_inv_predicate env evdref indf realargs id status concl in
     let sigma = !evdref in
     let (cut_concl,case_tac) =
-      if status != NoDep && (dependent sigma (EConstr.of_constr c) (EConstr.of_constr concl)) then
-        Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
+      if status != NoDep && (dependent sigma c concl) then
+        Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
         case_then_using
       else
-        Reduction.beta_appvect elim_predicate (Array.of_list realargs),
+        Reductionops.beta_applist sigma (elim_predicate, realargs),
         case_nodep_then_using
     in
     let cut_concl = EConstr.of_constr cut_concl in
     let refined id =
       let prf = mkApp (mkVar id, args) in
-      let prf = EConstr.of_constr prf in
       Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
-    let elim_predicate = EConstr.of_constr elim_predicate in
     let tac =
       (tclTHENS
         (assert_before Anonymous cut_concl)
         [case_tac names
             (introCaseAssumsThen false (* ApplyOn not supported by inversion *)
                (rewrite_equations_tac as_mode inv_kind id neqns))
-            (Some elim_predicate) ind (EConstr.of_constr c,t);
+            (Some elim_predicate) ind (c,t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
     in
     Sigma.Unsafe.of_pair (tac, sigma)
@@ -513,7 +510,7 @@ let inv k = inv_gen k NoDep
 let inv_tac id       = inv FullInversion None (NamedHyp id)
 let inv_clear_tac id = inv FullInversionClear None (NamedHyp id)
 
-let dinv k c = inv_gen k (Dep (Option.map EConstr.Unsafe.to_constr c))
+let dinv k c = inv_gen k (Dep c)
 
 let dinv_tac id       = dinv FullInversion None None (NamedHyp id)
 let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 6bb2b7282..446a62f6d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open EConstr
 open Misctypes
 open Tactypes
 
@@ -20,7 +21,7 @@ val inv_clause :
 val inv : inversion_kind -> or_and_intro_pattern option ->
   quantified_hypothesis -> unit Proofview.tactic
 
-val dinv : inversion_kind -> EConstr.constr option ->
+val dinv : inversion_kind -> constr option ->
   or_and_intro_pattern option -> quantified_hypothesis -> unit Proofview.tactic
 
 val inv_tac : Id.t -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b9da11021..bae1ad48c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4367,6 +4367,7 @@ let clear_unselected_context id inhyps cls =
 
 let use_bindings env sigma elim must_be_closed (c,lbind) typ =
   let sigma = Sigma.to_evar_map sigma in
+  let typ = EConstr.of_constr typ in
   let typ =
     if elim == None then
       (* w/o an scheme, the term has to be applied at least until
@@ -4374,7 +4375,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
          known only by pattern-matching, as in the case of a term of
          the form "nat_rect ?A ?o ?s n", with ?A to be inferred by
          matching. *)
-      let sign,t = splay_prod env sigma (EConstr.of_constr typ) in it_mkProd t sign
+      let sign,t = splay_prod env sigma typ in it_mkProd t sign
     else
       (* Otherwise, we exclude the case of an induction argument in an
          explicitly functional type. Henceforth, we can complete the
@@ -4384,7 +4385,6 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
       typ in
   let rec find_clause typ =
     try
-      let typ = EConstr.of_constr typ in
       let indclause = make_clenv_binding env sigma (c,typ) lbind in
       if must_be_closed && occur_meta indclause.evd (clenv_value indclause) then
         error "Need a fully applied argument.";
@@ -4392,7 +4392,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
       let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
       Sigma.Unsafe.of_pair (c, sigma)
     with e when catchable_exception e ->
-    try find_clause (try_red_product env sigma (EConstr.of_constr typ))
+    try find_clause (EConstr.of_constr (try_red_product env sigma typ))
     with Redelimination -> raise e in
   find_clause typ