Tactics API using EConstr.

13 files changed, 44 insertions, 44 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 57d12a19f6..360199fecb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -297,7 +297,7 @@ let inductive_template evdref env tmloc ind =
         | LocalAssum (na,ty) ->
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
-	    let e = EConstr.of_constr (e_new_evar env evdref ~src:(hole_source n) ty') in
+	    let e = e_new_evar env evdref ~src:(hole_source n) ty' in
 	    (e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
             let b = EConstr.of_constr b in
@@ -380,7 +380,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref =
-  let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in EConstr.of_constr e
+  let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
 
 let evd_comb2 f evdref x y =
   let (evd',y) = f !evdref x y in
@@ -1663,7 +1663,6 @@ let abstract_tycon loc env evdref subst tycon extenv t =
               1 (rel_context env) in
         let ty = EConstr.of_constr ty in
         let ev' = e_new_evar env evdref ~src ty in
-        let ev' = EConstr.of_constr ev' in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1698,7 +1697,6 @@ let abstract_tycon loc env evdref subst tycon extenv t =
       let candidates = u :: List.map mkRel vl in
       let candidates = List.map EConstr.Unsafe.to_constr candidates in
       let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
-      let ev = EConstr.of_constr ev in
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1712,7 +1710,6 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 	let n' = Context.Rel.length (rel_context tycon_env) in
 	let impossible_case_type, u =
 	  e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in
-        let impossible_case_type = EConstr.of_constr impossible_case_type in
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
@@ -2010,7 +2007,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
           let Sigma ((t, _), sigma, _) =
 	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
           let sigma = Sigma.to_evar_map sigma in
-	    sigma, EConstr.of_constr t
+	    sigma, t
 	in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9011186a3d..23d20dad3e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -51,6 +51,7 @@ type coe_info_typ = {
   coe_param : int }
 
 let coe_info_typ_equal c1 c2 =
+  let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in
   eq_constr c1.coe_value c2.coe_value &&
     eq_constr c1.coe_type c2.coe_type &&
     c1.coe_local == c2.coe_local &&
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e7279df7a5..d67976232a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -93,7 +93,7 @@ open Program
 
 let make_existential loc ?(opaque = not (get_proofs_transparency ()))  env evdref c =
   let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
-  EConstr.of_constr (Evarutil.e_new_evar env evdref ~src c)
+  Evarutil.e_new_evar env evdref ~src c
 
 let app_opt env evdref f t =
   EConstr.of_constr (whd_betaiota !evdref (app_opt f t))
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4756ec30e7..ec8945e85e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -294,7 +294,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | na::nal ->
     match kind_of_term c with
     | Case (ci,p,c,cl) when
-        eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
+        eq_constr sigma (EConstr.of_constr c) (EConstr.mkRel (List.index Name.equal na (fst (snd e))))
         && not (Int.equal (Array.length cl) 0)
 	&& (* don't contract if p dependent *)
 	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ee6355736b..a968af7ff2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -890,7 +890,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	    let i = Sigma.Unsafe.of_evar_map i in
             let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
             let i' = Sigma.to_evar_map i' in
-	    (i', EConstr.of_constr ev :: ks, m - 1,test))
+	    (i', ev :: ks, m - 1,test))
 	(evd,[],List.length bs,fun i -> Success i) bs
     in
     let app = mkApp (c, Array.rev_of_list ks) in
@@ -1066,13 +1066,13 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | Some _ -> error "Selection of specific occurrences not supported"
         | None ->
         let evty = set_holes evdref cty subst in
-        let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in
+        let instance = Filter.filter_list filter instance in
         let evd = Sigma.Unsafe.of_evar_map !evdref in
         let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
         let evd = Sigma.to_evar_map evd in
         evdref := evd;
-        evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref;
-        EConstr.of_constr ev in
+        evsref := (fst (destEvar !evdref ev),evty)::!evsref;
+        ev in
       set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
   | [] -> rhs in
 
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index fa3b9ca0b7..3babc48a7f 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -22,6 +22,11 @@ open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
+let nlocal_assum (na, t) =
+  let open Context.Named.Declaration in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
 let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
@@ -88,7 +93,7 @@ let define_pure_evar_as_product evd evk =
     (Sigma.to_evar_map evd1, e)
   in
   let evd2,rng =
-    let newenv = push_named (LocalAssum (id, dom)) evenv in
+    let newenv = push_named (nlocal_assum (id, dom)) evenv in
     let src = evar_source evk evd1 in
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort s then
@@ -105,8 +110,7 @@ let define_pure_evar_as_product evd evk =
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
 	  evd3, rng
   in
-  let rng = EConstr.of_constr rng in
-  let prod = mkProd (Name id, EConstr.of_constr dom, subst_var id rng) in
+  let prod = mkProd (Name id, dom, subst_var id rng) in
   let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in
     evd3,prod
 
@@ -140,14 +144,13 @@ let define_pure_evar_as_lambda env evd evk =
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
   | _ -> error_not_product env evd typ in
   let avoid = ids_of_named_context (evar_context evi) in
-  let dom = EConstr.Unsafe.to_constr dom in
   let id =
-    next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
-  let newenv = push_named (LocalAssum (id, dom)) evenv in
+    next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd (EConstr.Unsafe.to_constr dom)) in
+  let newenv = push_named (nlocal_assum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
   let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
-  let lam = mkLambda (Name id, EConstr.of_constr dom, subst_var id (EConstr.of_constr body)) in
+  let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
 
 let define_evar_as_lambda env evd (evk,args) =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b7db51d5c5..4ce8a44adc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -518,15 +518,15 @@ let is_unification_pattern (env,nb) evd f l t =
 let solve_pattern_eqn env sigma l c =
   let c' = List.fold_right (fun a c ->
     let c' = subst_term sigma (lift 1 a) (lift 1 c) in
+    let c' = EConstr.of_constr c' in
     match EConstr.kind sigma a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
           let open Context.Rel.Declaration in
           let d = map_constr (CVars.lift n) (lookup_rel n env) in
-          let c' = EConstr.of_constr c' in
           mkLambda_or_LetIn d c'
       | Var id ->
-          let d = lookup_named id env in EConstr.of_constr (mkNamedLambda_or_LetIn d c')
+          let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
       | _ -> assert false)
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
@@ -592,10 +592,9 @@ let make_projectable_subst aliases sigma evi args =
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src inst_in_env in
   let evd = Sigma.to_evar_map evd in
   let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
-  let evar_in_env = EConstr.of_constr evar_in_env in
   let (evk, _) = destEvar evd evar_in_env in
   let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -669,10 +668,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in
   let Sigma (ev2_in_sign, evd, _) =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src (List.map EConstr.Unsafe.to_constr inst2_in_sign) in
+    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
   let evd = Sigma.to_evar_map evd in
-  let ev2_in_env = (fst (destEvar evd (EConstr.of_constr ev2_in_sign)), Array.of_list inst2_in_env) in
-  (evd, EConstr.of_constr ev2_in_sign, ev2_in_env)
+  let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in
+  (evd, ev2_in_sign, ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
   let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e30ba21fd1..98b267cfd4 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -556,6 +556,7 @@ let set_pattern_names env ind brv =
 
 let type_case_branches_with_names env sigma indspec p c =
   let (ind,args) = indspec in
+  let args = List.map EConstr.Unsafe.to_constr args in
   let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
   let nparams = mib.mind_nparams in
   let (params,realargs) = List.chop nparams args in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cf5523a50d..7af9731f9a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -175,7 +175,7 @@ val arity_of_case_predicate :
   env -> inductive_family -> bool -> sorts -> types
 
 val type_case_branches_with_names :
-  env -> evar_map -> pinductive * constr list -> constr -> constr -> types array * types
+  env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types
 
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 49a0bccee9..7586b54ba1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -116,7 +116,7 @@ let lookup_named id env = lookup_named id env.env
 let e_new_evar env evdref ?src ?naming typ =
   let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
   let open Context.Named.Declaration in
-  let inst_vars = List.map (get_id %> Constr.mkVar) (named_context env.env) in
+  let inst_vars = List.map (get_id %> EConstr.mkVar) (named_context env.env) in
   let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
   let (subst, vsubst, _, nc) = Lazy.force env.extra in
   let typ' = subst2 subst vsubst typ in
@@ -125,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ =
   let sigma = Sigma.Unsafe.of_evar_map !evdref in
   let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in
   evdref := Sigma.to_evar_map sigma;
-  EConstr.of_constr e
+  e
 
 let push_rec_types (lna,typarray,_) env =
   let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in
@@ -546,7 +546,7 @@ let new_type_evar env evdref loc =
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
   in
   evdref := Sigma.to_evar_map sigma;
-  EConstr.of_constr e
+  e
 
 let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 24d4af89a6..1ec8deb1b5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1196,7 +1196,7 @@ let reduce_to_ind_gen allow_product env sigma t =
     let t = hnf_constr env sigma t in
     let t = EConstr.of_constr t in
     match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) with
-      | Ind ind-> (check_privacy env ind, EConstr.Unsafe.to_constr (it_mkProd_or_LetIn t l))
+      | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
       | Prod (n,ty,t') ->
 	  let open Context.Rel.Declaration in
 	  if allow_product then
@@ -1209,7 +1209,7 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  let t' = whd_all env sigma t in
 	  let t' = EConstr.of_constr t' in
 	  match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t'))) with
-	    | Ind ind-> (check_privacy env ind, EConstr.Unsafe.to_constr (it_mkProd_or_LetIn t' l))
+	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
 	    | _ -> user_err  (str"Not an inductive product.")
   in
   elimrec env t []
@@ -1219,7 +1219,7 @@ let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma c
 
 let find_hnf_rectype env sigma t =
   let ind,t = reduce_to_atomic_ind env sigma t in
-  ind, snd (Term.decompose_app t)
+  ind, snd (decompose_app sigma t)
 
 (* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta]
    or raise [NotStepReducible] if not a weak-head redex *)
@@ -1295,7 +1295,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
             elimrec env t' l
           with NotStepReducible -> error_cannot_recognize ref
   in
-  EConstr.Unsafe.to_constr (elimrec env t [])
+  elimrec env t []
 
 let reduce_to_quantified_ref = reduce_to_ref_gen true
 let reduce_to_atomic_ref = reduce_to_ref_gen false
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 3587ae2810..15b4e990d8 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -75,23 +75,23 @@ val cbv_norm_flags : CClosure.RedFlags.reds ->  reduction_function
 (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_atomic_ind : env ->  evar_map -> EConstr.types -> pinductive * types
+val reduce_to_atomic_ind : env ->  evar_map -> EConstr.types -> pinductive * EConstr.types
 
 (** [reduce_to_quantified_ind env sigma t] puts [t] in the form
    [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_quantified_ind : env ->  evar_map -> EConstr.types -> pinductive * types
+val reduce_to_quantified_ind : env ->  evar_map -> EConstr.types -> pinductive * EConstr.types
 
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
-  env ->  evar_map -> global_reference -> EConstr.types -> types
+  env ->  evar_map -> global_reference -> EConstr.types -> EConstr.types
 
 val reduce_to_atomic_ref :
-  env ->  evar_map -> global_reference -> EConstr.types -> types
+  env ->  evar_map -> global_reference -> EConstr.types -> EConstr.types
 
 val find_hnf_rectype : 
-  env ->  evar_map -> EConstr.types -> pinductive * constr list
+  env ->  evar_map -> EConstr.types -> pinductive * EConstr.constr list
 
 val contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> reduction_function) -> reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2b2069ec45..bc59a41087 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -133,14 +133,14 @@ let abstract_list_all_with_dependencies env evd typ c l =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (ev, evd, _) = new_evar env evd typ in
   let evd = Sigma.to_evar_map evd in
-  let evd,ev' = evar_absorb_arguments env evd (destEvar evd (EConstr.of_constr ev)) l in
+  let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in
   let n = List.length l in
   let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
   let evd,b =
     Evarconv.second_order_matching empty_transparent_state
       env evd ev' argoccs c in
   if b then
-    let p = nf_evar evd ev in
+    let p = nf_evar evd (EConstr.Unsafe.to_constr ev) in
       evd, p
   else error_cannot_find_well_typed_abstraction env evd 
     c l None
@@ -184,8 +184,8 @@ let pose_all_metas_as_evars env evd t =
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
         let src = Evd.evar_source_of_meta mv !evdref in
         let ev = Evarutil.e_new_evar env evdref ~src ty in
-        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
-        EConstr.of_constr ev)
+        evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
+        ev)
   | _ ->
       EConstr.map !evdref aux t in
   let c = aux t in
@@ -1236,7 +1236,6 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
       match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma cty)) with
       | Prod (_,c1,c2) ->
         let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
-        let evar = EConstr.of_constr evar in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
       | _ -> error "Apply_Head_Then"
   in