Inv API using EConstr.

15 files changed, 61 insertions, 50 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index c2d862f00..4ab9f0733 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -224,8 +224,8 @@ let mkProd_wo_LetIn decl c =
     | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c)
     | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c
 
-let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
-let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
+let it_mkProd init = List.fold_left (fun c (n,t)  -> EConstr.mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t)  -> EConstr.mkLambda (n, t, c)) init
 
 let it_named_context_quantifier f ~init =
   List.fold_left (fun c d -> f d c) init
diff --git a/engine/termops.mli b/engine/termops.mli
index 013efcbcb..1c14e6c89 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -46,8 +46,8 @@ val rel_list : int -> int -> EConstr.constr list
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
 val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.types
-val it_mkProd : types -> (Name.t * types) list -> types
-val it_mkLambda : constr -> (Name.t * types) list -> constr
+val it_mkProd : EConstr.types -> (Name.t * EConstr.types) list -> EConstr.types
+val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.constr
 val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
 val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types
 val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 0d279ae93..f2ffb0413 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -39,6 +39,10 @@ open Context.Named.Declaration
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  RelDecl.LocalAssum (na, inj t)
+
 (** Typeclass-based generalized rewriting. *)
 
 (** Constants used by the tactic. *)
@@ -531,7 +535,8 @@ let decompose_applied_relation env sigma (c,l) =
     | Some c -> c
     | None ->
 	let ctx,t' = Reductionops.splay_prod env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
-	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
+	let t' = EConstr.Unsafe.to_constr t' in
+	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> local_assum (n, t)) ctx)) with
 	| Some c -> c
 	| None -> error "Cannot find an homogeneous relation to rewrite."
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6559aeb08..e9fd40722 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -325,6 +325,7 @@ and extract_type_scheme env db c p =
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
       | _ ->
           let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in
+          let rels = List.map (on_snd EConstr.Unsafe.to_constr) rels in
           let env = push_rels_assum rels env in
           let eta_args = List.rev_map mkRel (List.interval 1 p) in
           extract_type env db 0 (lift p c) eta_args
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ff3424c44..cdaa4e9ee 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -99,6 +99,8 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
   let build_one_branch i cty =
     let typi = type_constructor mind mib u cty params in
     let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
+    let decl = List.map (on_snd EConstr.Unsafe.to_constr) decl in
+    let indapp = EConstr.Unsafe.to_constr indapp in
     let decl_with_letin,_ = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f09f3221d..3230f92da 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -203,7 +203,8 @@ let compute_canonical_projections warn (con,ind) =
   let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
   let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
-  let lt = List.rev_map snd lt in
+  let t = EConstr.Unsafe.to_constr t in
+  let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
@@ -303,6 +304,7 @@ let check_and_decompose_canonical_structure ref =
     | Some vc -> vc
     | None -> error_not_structure ref in
   let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
+  let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind_of_term body with
     | App (f,args) -> f,args
     | _ -> error_not_structure ref in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0dd615bfb..480ec2319 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1453,13 +1453,13 @@ let hnf_lam_applist env sigma t nl =
   List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let bind_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  (na, inj t)
+  (na, t)
 
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
@@ -1470,7 +1470,8 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
@@ -1498,7 +1499,7 @@ let splay_prod_assum env sigma =
 
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
-  match EConstr.kind sigma (EConstr.of_constr c) with
+  match EConstr.kind sigma c with
     | Sort s -> l,s
     | _ -> invalid_arg "splay_arity"
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 864b1a625..e67fad3fd 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -213,9 +213,9 @@ val hnf_lam_app      : env ->  evar_map -> EConstr.t -> EConstr.t -> constr
 val hnf_lam_appvect  : env ->  evar_map -> EConstr.t -> EConstr.t array -> constr
 val hnf_lam_applist  : env ->  evar_map -> EConstr.t -> EConstr.t list -> constr
 
-val splay_prod : env ->  evar_map -> EConstr.t -> (Name.t * constr) list * constr
-val splay_lam : env ->  evar_map -> EConstr.t -> (Name.t * constr) list * constr
-val splay_arity : env ->  evar_map -> EConstr.t -> (Name.t * constr) list * sorts
+val splay_prod : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
+val splay_lam : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
+val splay_arity : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts
 val sort_of_arity : env -> evar_map -> EConstr.t -> sorts
 val splay_prod_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
 val splay_lam_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 60f99fd3d..31693d82f 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -106,6 +106,8 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
   let build_one_branch i cty =
     let typi = type_constructor mind mib u cty params in
     let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
+    let decl = List.map (on_snd EConstr.Unsafe.to_constr) decl in
+    let indapp = EConstr.Unsafe.to_constr indapp in
     let decl_with_letin,_ = decompose_prod_assum typi in
     let ((ind,u),cargs) = find_rectype_a env indapp in
     let nparams = Array.length params in
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