From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 tactics/equality.ml | 41 +++++++++++++++++++++++------------------
 1 file changed, 23 insertions(+), 18 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c819edadc..74f6dd44ae 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -405,7 +405,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let isatomic = isProd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
-  let dep = dep_proof_ok && dep_fun c type_of_cls in
+  let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
   let tac =
       Proofview.tclEFFECTS effs <*>
@@ -442,7 +442,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
-      match match_with_equality_type t with
+      match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
@@ -455,9 +455,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
             end
             begin function
               | (e, info) ->
+                  Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
-	          match match_with_equality_type t' with
+	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
@@ -932,9 +933,10 @@ let rec build_discriminator env sigma dirn c = function
 
 let gen_absurdity id =
   Proofview.Goal.enter { enter = begin fun gl ->
+  let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
   let hyp_typ = pf_nf_evar gl hyp_typ in
-  if is_empty_type hyp_typ
+  if is_empty_type sigma hyp_typ
   then
     simplest_elim (mkVar id)
   else
@@ -973,7 +975,7 @@ let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
+    (match kind_of_term (last_arg f_clause.evd (EConstr.of_constr f_clause.templval.Evd.rebus)) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
@@ -1025,7 +1027,7 @@ let onNegatedEquality with_evars tac =
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     match kind_of_term (hnf_constr env sigma ccl) with
-    | Prod (_,t,u) when is_empty_type u ->
+    | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
@@ -1079,7 +1081,7 @@ let find_sigma_data env s = build_sigma_type ()
  *)
 
 let make_tuple env sigma (rterm,rty) lind =
-  assert (dependent (mkRel lind) rty);
+  assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
@@ -1101,9 +1103,9 @@ let make_tuple env sigma (rterm,rty) lind =
    normalization *)
 
 let minimal_free_rels env sigma (c,cty) =
-  let cty_rels = free_rels cty in
+  let cty_rels = free_rels sigma (EConstr.of_constr cty) in
   let cty' = simpl env sigma cty in
-  let rels' = free_rels cty' in
+  let rels' = free_rels sigma (EConstr.of_constr cty') in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
   else
@@ -1302,6 +1304,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 let inject_if_homogenous_dependent_pair ty =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   try
+    let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
@@ -1310,8 +1313,8 @@ let inject_if_homogenous_dependent_pair ty =
     (* check whether the equality deals with dep pairs or not *)
     let eqTypeDest = fst (decompose_app t) in
     if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
-    let hd1,ar1 = decompose_app_vect t1 and
-        hd2,ar2 = decompose_app_vect t2 in
+    let hd1,ar1 = decompose_app_vect sigma (EConstr.of_constr t1) and
+        hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr t2) in
     if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
     if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
     let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
@@ -1543,7 +1546,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term e body)) e1_list b in
+      (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
   let pred_body = beta_applist(abst_B,proj_list) in
   let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist (abst_B,List.map fst e2_list) in
@@ -1674,8 +1677,8 @@ let is_eq_x gl x d =
     in
     let c = pf_nf_evar gl (NamedDecl.get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
-    if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
+    if (is_var x lhs) && not (local_occur_var (project gl) x (EConstr.of_constr rhs)) then raise (FoundHyp (id,rhs,true));
+    if (is_var x rhs) && not (local_occur_var (project gl) x (EConstr.of_constr lhs)) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
     ()
 
@@ -1685,6 +1688,7 @@ let is_eq_x gl x d =
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
@@ -1692,7 +1696,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
     List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
       let id = NamedDecl.get_id dcl in
       if not (Id.equal id hyp)
-         && List.exists (fun y -> occur_var_in_decl env y dcl) deps
+         && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps
       then
         let id_dest = if !regular_subst_tactic then dest else MoveLast in
         (dest,id::deps,(id_dest,id)::allhyps)
@@ -1701,7 +1705,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       hyps
       (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
-  let depconcl = occur_var env x concl in
+  let depconcl = occur_var env sigma x (EConstr.of_constr concl) in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
@@ -1787,6 +1791,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let process hyp =
     Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
+    let sigma = project gl in
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
@@ -1794,9 +1799,9 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if Term.eq_constr x y then Proofview.tclUNIT () else
       match kind_of_term x, kind_of_term y with
-      | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) ->
+      | Var x', _ when not (occur_term sigma (EConstr.of_constr x) (EConstr.of_constr y)) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (occur_term sigma (EConstr.of_constr y) (EConstr.of_constr x)) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
-- 
cgit v1.2.3


From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 tactics/equality.ml | 60 +++++++++++++++++++++++++++--------------------------
 1 file changed, 31 insertions(+), 29 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 74f6dd44ae..48f46b36be 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -328,7 +328,7 @@ let jmeq_same_dom gl = function
   | Some t ->
     let rels, t = decompose_prod_assum t in
     let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
-    match decompose_app t with
+    match EConstr.decompose_app (project gl) (EConstr.of_constr t) with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
 
@@ -402,7 +402,7 @@ let type_of_clause cls gl = match cls with
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-  let isatomic = isProd (whd_zeta evd hdcncl) in
+  let isatomic = isProd (whd_zeta evd (EConstr.of_constr hdcncl)) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
@@ -441,7 +441,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
-    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
+    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in
       match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -457,7 +457,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
               | (e, info) ->
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
-	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+	          let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *)
 	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -714,9 +714,11 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-
 let find_positions env sigma t1 t2 =
+  let open EConstr in
   let project env sorts posn t1 t2 =
+    let t1 = EConstr.Unsafe.to_constr t1 in
+    let t2 = EConstr.Unsafe.to_constr t2 in
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
     if Sorts.List.mem s sorts
@@ -725,7 +727,7 @@ let find_positions env sigma t1 t2 =
   let rec findrec sorts posn t1 t2 =
     let hd1,args1 = whd_all_stack env sigma t1 in
     let hd2,args2 = whd_all_stack env sigma t2 in
-    match (kind_of_term hd1, kind_of_term hd2) with
+    match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with
       | Construct (sp1,_), Construct (sp2,_)
           when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
             ->
@@ -760,7 +762,7 @@ let find_positions env sigma t1 t2 =
     let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
 		else [InSet;InType]
     in
-    Inr (findrec sorts [] t1 t2)
+    Inr (findrec sorts [] (EConstr.of_constr t1) (EConstr.of_constr t2))
   with DiscrFound (path,c1,c2) ->
     Inl (path,c1,c2)
 
@@ -840,7 +842,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (get_type_of env sigma head)
+    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -883,7 +885,7 @@ let descend_then env sigma head dirn =
 
 let build_selector env sigma dirn c ind special default =
   let IndType(indf,_) =
-    try find_rectype env sigma ind
+    try find_rectype env sigma (EConstr.of_constr ind)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors
           like T := c : (A:Set)A->T and a discrimination
@@ -1026,7 +1028,7 @@ let onNegatedEquality with_evars tac =
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    match kind_of_term (hnf_constr env sigma ccl) with
+    match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with
     | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
@@ -1104,7 +1106,7 @@ let make_tuple env sigma (rterm,rty) lind =
 
 let minimal_free_rels env sigma (c,cty) =
   let cty_rels = free_rels sigma (EConstr.of_constr cty) in
-  let cty' = simpl env sigma cty in
+  let cty' = simpl env sigma (EConstr.of_constr cty) in
   let rels' = free_rels sigma (EConstr.of_constr cty') in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
@@ -1171,11 +1173,11 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with Evarconv.UnableToUnify _ ->
 	error "Cannot solve a unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
-	| (_sigS,[a;p]) -> (a,p)
+      let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with
+	| (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
       let ev = Evarutil.e_new_evar env evdref a in
-      let rty = beta_applist(p_i_minus_1,[ev]) in
+      let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[EConstr.of_constr ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
         Evd.existential_opt_value !evdref
@@ -1317,13 +1319,13 @@ let inject_if_homogenous_dependent_pair ty =
         hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr t2) in
     if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
     if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
+    let ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr ar1.(0)) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
-      pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
+      pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
@@ -1350,8 +1352,8 @@ let inject_if_homogenous_dependent_pair ty =
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
   match decompose_app t with
-    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
-    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
+    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma (EConstr.of_constr c1);simpl env sigma (EConstr.of_constr c2)])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma (EConstr.of_constr c1);t2;simpl env sigma (EConstr.of_constr c2)])
     | _ -> t
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
@@ -1515,14 +1517,14 @@ let _ = declare_intro_decomp_eq intro_decomp_eq
 
  *)
 
-let decomp_tuple_term env c t =
+let decomp_tuple_term env sigma c t =
   let rec decomprec inner_code ex exty =
     let iterated_decomp =
     try
       let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose ex in
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
-      let cdrtyp = beta_applist (p,[car]) in
+      let cdrtyp = beta_applist sigma (EConstr.of_constr p,[EConstr.of_constr car]) in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
@@ -1533,8 +1535,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
   (* We find all possible decompositions *)
-  let decomps1 = decomp_tuple_term env dep_pair1 typ in
-  let decomps2 = decomp_tuple_term env dep_pair2 typ in
+  let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
+  let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
   (* We adjust to the shortest decomposition *)
   let n = min (List.length decomps1) (List.length decomps2) in
   let decomp1 = List.nth decomps1 (n-1) in
@@ -1547,11 +1549,11 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let abst_B =
     List.fold_right
       (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
-  let pred_body = beta_applist(abst_B,proj_list) in
+  let pred_body = beta_applist sigma (EConstr.of_constr abst_B, List.map EConstr.of_constr proj_list) in
   let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
-  let expected_goal = beta_applist (abst_B,List.map fst e2_list) in
+  let expected_goal = beta_applist sigma (EConstr.of_constr abst_B,List.map (fst %> EConstr.of_constr) e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
-  let expected_goal = nf_betaiota sigma expected_goal in
+  let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
   (* Retype to get universes right *)
   let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
@@ -1842,20 +1844,20 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 let cond_eq_term_left c t gl =
   try
     let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then true else failwith "not convertible"
+    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
     let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then false else failwith "not convertible"
+    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
     let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then true
-    else if pf_conv_x gl c y then false
+    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true
+    else if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr y) then false
     else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
-- 
cgit v1.2.3


From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Nov 2016 14:48:36 +0100
Subject: Retyping API using EConstr.

---
 tactics/equality.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 48f46b36be..e87746a28e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -440,7 +440,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     Proofview.Goal.enter { enter = begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
-    let ctype = get_type_of env sigma c in
+    let ctype = get_type_of env sigma (EConstr.of_constr c) in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in
       match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
@@ -621,8 +621,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
   let get_type_of = pf_apply get_type_of gl in
-  let t1 = get_type_of c1
-  and t2 = get_type_of c2 in
+  let t1 = get_type_of (EConstr.of_constr c1)
+  and t2 = get_type_of (EConstr.of_constr c2) in
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
@@ -719,8 +719,8 @@ let find_positions env sigma t1 t2 =
   let project env sorts posn t1 t2 =
     let t1 = EConstr.Unsafe.to_constr t1 in
     let t2 = EConstr.Unsafe.to_constr t2 in
-    let ty1 = get_type_of env sigma t1 in
-    let s = get_sort_family_of env sigma ty1 in
+    let ty1 = get_type_of env sigma (EConstr.of_constr t1) in
+    let s = get_sort_family_of env sigma (EConstr.of_constr ty1) in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
   in
@@ -842,7 +842,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
+    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma (EConstr.of_constr head)))
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -897,7 +897,7 @@ let build_selector env sigma dirn c ind special default =
 		 dependent types.") in
   let (indp,_) = dest_ind_family indf in
   let ind, _ = check_privacy env indp in
-  let typ = Retyping.get_type_of env sigma default in
+  let typ = Retyping.get_type_of env sigma (EConstr.of_constr default) in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
@@ -912,7 +912,7 @@ let build_selector env sigma dirn c ind special default =
 
 let rec build_discriminator env sigma dirn c = function
   | [] ->
-      let ind = get_type_of env sigma c in
+      let ind = get_type_of env sigma (EConstr.of_constr c) in
       let true_0,false_0 =
         build_coq_True(),build_coq_False() in
       build_selector env sigma dirn c ind true_0 false_0
@@ -1084,7 +1084,7 @@ let find_sigma_data env s = build_sigma_type ()
 
 let make_tuple env sigma (rterm,rty) lind =
   assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
-  let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
+  let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
@@ -1262,7 +1262,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
-  let sort_of_zty = get_sort_of env sigma zty in
+  let sort_of_zty = get_sort_of env sigma (EConstr.of_constr zty) in
   let sorted_rels = Int.Set.elements rels in
   let sigma, (tuple,tuplety) =
     List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels
@@ -1533,7 +1533,7 @@ let decomp_tuple_term env sigma c t =
 
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
-  let typ = get_type_of env sigma dep_pair1 in
+  let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
   let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
@@ -1623,7 +1623,7 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let eq = pf_apply get_type_of gl c in
+  let eq = pf_apply get_type_of gl (EConstr.of_constr c) in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
-- 
cgit v1.2.3


From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 03:23:13 +0100
Subject: Evarconv API using EConstr.

---
 tactics/equality.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index e87746a28e..17038e42d1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -626,7 +626,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
+      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) (EConstr.of_constr t1) (EConstr.of_constr t2) (Tacmach.New.project gl))
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -1167,7 +1167,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       (* is the default value typable with the expected type *)
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
-	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
+	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
@@ -1185,7 +1185,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with
 	| Some w ->
             let w_type = unsafe_type_of env sigma w in
-            if Evarconv.e_cumul env evdref w_type a then
+            if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
-- 
cgit v1.2.3


From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 17:21:44 +0100
Subject: Typing API using EConstr.

---
 tactics/equality.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 17038e42d1..58c86ff426 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1085,7 +1085,7 @@ let find_sigma_data env s = build_sigma_type ()
 let make_tuple env sigma (rterm,rty) lind =
   assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
   let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
-  let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+  let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1119,7 +1119,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.mkRel i)))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1165,7 +1165,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = unsafe_type_of env sigma dflt in
+      let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
@@ -1184,7 +1184,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
           (destEvar ev)
       with
 	| Some w ->
-            let w_type = unsafe_type_of env sigma w in
+            let w_type = unsafe_type_of env sigma (EConstr.of_constr w) in
             if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
@@ -1273,7 +1273,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
+  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c))
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1367,7 +1367,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
-      let sigma, pf_typ = Typing.type_of env sigma pf in
+      let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1555,8 +1555,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
   (* Retype to get universes right *)
-  let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
-  let sigma, _ = Typing.type_of env sigma body in
+  let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in
+  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in
   Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
 
 (* Like "replace" but decompose dependent equalities                      *)
-- 
cgit v1.2.3


From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 10:57:05 +0100
Subject: Cases API using EConstr.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58c86ff426..9679ac4026 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -864,7 +864,7 @@ let descend_then env sigma head dirn =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl)))
+      EConstr.Unsafe.to_constr (Inductiveops.make_case_or_project env sigma indf ci (EConstr.of_constr p) (EConstr.of_constr head) (Array.map_of_list EConstr.of_constr brl))))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
-- 
cgit v1.2.3


From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 19:02:40 +0100
Subject: Pretyping API using EConstr.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9679ac4026..be175937ba 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1176,7 +1176,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with
 	| (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
-      let ev = Evarutil.e_new_evar env evdref a in
+      let ev = Evarutil.e_new_evar env evdref (EConstr.of_constr a) in
       let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[EConstr.of_constr ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-- 
cgit v1.2.3


From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Nov 2016 11:39:27 +0100
Subject: Unification API using EConstr.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index be175937ba..64b56b99bc 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -177,7 +177,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
     w_unify_to_subterm_all ~flags env eqclause.evd
-      ((if l2r then c1 else c2),concl)
+      (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr concl)
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-- 
cgit v1.2.3


From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

---
 tactics/equality.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 64b56b99bc..ad80d2d1fb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -181,8 +181,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let sigma, ct = pf_type_of gl c in
-  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+  let sigma, ct = pf_type_of gl (EConstr.of_constr c) in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -992,6 +992,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
+  let pf = EConstr.of_constr pf in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
@@ -1012,8 +1013,8 @@ let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
-  let t = type_of c in
-  let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
+  let t = type_of (EConstr.of_constr c) in
+  let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
@@ -1327,7 +1328,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr ar1.(3));ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
@@ -1339,7 +1340,7 @@ let inject_if_homogenous_dependent_pair ty =
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar hyp];
            Proofview.V82.tactic (Tacmach.refine
-             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
+             (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1384,7 +1385,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (Tacmach.refine pf)])
+            Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
-- 
cgit v1.2.3


From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 tactics/equality.ml | 38 ++++++++++++++++++++++++++------------
 1 file changed, 26 insertions(+), 12 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ad80d2d1fb..fbf461f6f8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -144,7 +144,7 @@ let freeze_initial_evars sigma flags clause =
   (* We take evars of the type: this may include old evars! For excluding *)
   (* all old evars, including the ones occurring in the rewriting lemma, *)
   (* we would have to take the clenv_value *)
-  let newevars = Evd.evars_of_term (clenv_type clause) in
+  let newevars = Evd.evars_of_term (EConstr.Unsafe.to_constr (clenv_type clause)) in
   let evars =
     fold_undefined (fun evk _ evars ->
       if Evar.Set.mem evk newevars then evars
@@ -165,8 +165,11 @@ let side_tac tac sidetac =
 
 let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let env = Proofview.Goal.env gl in
+  let c = EConstr.of_constr c in
+  let ty = EConstr.of_constr ty in
+  let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
-  let (equiv, args) = decompose_appvect (Clenv.clenv_type eqclause) in
+  let (equiv, args) = decompose_appvect (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
   let arglen = Array.length args in
   let () = if arglen < 2 then error "The term provided is not an applied relation." in
   let c1 = args.(arglen - 2) in
@@ -181,8 +184,11 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let sigma, ct = pf_type_of gl (EConstr.of_constr c) in
+  let c = EConstr.of_constr c in
+  let sigma, ct = pf_type_of gl c in
   let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
+  let t = EConstr.of_constr t in
+  let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -975,9 +981,11 @@ let eq_baseid = Id.of_string "e"
 
 let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
+  let f = EConstr.of_constr f in
+  let t = EConstr.of_constr t in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.evd (EConstr.of_constr f_clause.templval.Evd.rebus)) with
+    (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
@@ -992,7 +1000,6 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
-  let pf = EConstr.of_constr pf in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
@@ -1011,13 +1018,17 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let c = EConstr.of_constr c in
+  let lbindc = Miscops.map_bindings EConstr.of_constr lbindc in
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
-  let t = type_of (EConstr.of_constr c) in
+  let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
+  let t' = EConstr.of_constr t' in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
+  let eqn = EConstr.Unsafe.to_constr eqn in
   let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
@@ -1371,7 +1382,8 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
-      let ty = simplify_args env sigma (clenv_type inj_clause) in
+      let ty = simplify_args env sigma (EConstr.Unsafe.to_constr (clenv_type inj_clause)) in
+      let pf = EConstr.Unsafe.to_constr pf in
 	evdref := sigma;
 	Some (pf, ty)
     with Failure _ -> None
@@ -1405,7 +1417,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
      tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
-	(tac (clenv_value eq_clause))
+	(tac (EConstr.Unsafe.to_constr (clenv_value eq_clause)))
 
 let get_previous_hyp_position id gl =
   let rec aux dest = function
@@ -1464,10 +1476,10 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-        ntac (clenv_value clause) 0
+        ntac (EConstr.Unsafe.to_constr (clenv_value clause)) 0
     | Inr posns ->
 	inject_at_positions env sigma true u clause posns
-          (ntac (clenv_value clause))
+          (ntac (EConstr.Unsafe.to_constr (clenv_value clause)))
   end }
 
 let dEqThen with_evars ntac = function
@@ -1478,9 +1490,11 @@ let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
-let intro_decomp_eq tac data cl =
+let intro_decomp_eq tac data (c, t) =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let cl = pf_apply make_clenv_binding gl cl NoBindings in
+    let c = EConstr.of_constr c in
+    let t = EConstr.of_constr t in
+    let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
     decompEqThen (fun _ -> tac) data cl
   end }
 
-- 
cgit v1.2.3


From 45562afa065aadc207dca4e904e309d835cb66ef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:28:45 +0100
Subject: Tacticals API using EConstr.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fbf461f6f8..fa4164bb96 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -985,7 +985,7 @@ let apply_on_clause (f,t) clause =
   let t = EConstr.of_constr t in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
+    (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
-- 
cgit v1.2.3


From 771be16883c8c47828f278ce49545716918764c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:52:15 +0100
Subject: Hipattern API using EConstr.

---
 tactics/equality.ml | 72 +++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 50 insertions(+), 22 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fa4164bb96..e1a8d2bdb1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -448,8 +448,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma (EConstr.of_constr c) in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in
-      match match_with_equality_type sigma t with
+      match match_with_equality_type sigma (EConstr.of_constr t) with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
+          let hdcncl = EConstr.Unsafe.to_constr hdcncl in
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
 	    l with_evars frzevars dep_proof_ok hdcncl
@@ -464,8 +465,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *)
-	          match match_with_equality_type sigma t' with
+	          match match_with_equality_type sigma (EConstr.of_constr t') with
 	            | Some (hdcncl,args) ->
+                  let hdcncl = EConstr.Unsafe.to_constr hdcncl in
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
 		    (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
@@ -768,7 +770,7 @@ let find_positions env sigma t1 t2 =
     let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
 		else [InSet;InType]
     in
-    Inr (findrec sorts [] (EConstr.of_constr t1) (EConstr.of_constr t2))
+    Inr (findrec sorts [] t1 t2)
   with DiscrFound (path,c1,c2) ->
     Inl (path,c1,c2)
 
@@ -943,7 +945,7 @@ let gen_absurdity id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
-  let hyp_typ = pf_nf_evar gl hyp_typ in
+  let hyp_typ = EConstr.of_constr hyp_typ in
   if is_empty_type sigma hyp_typ
   then
     simplest_elim (mkVar id)
@@ -991,6 +993,9 @@ let apply_on_clause (f,t) clause =
   clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
+  let t = EConstr.Unsafe.to_constr t in
+  let t1 = EConstr.Unsafe.to_constr t1 in
+  let t2 = EConstr.Unsafe.to_constr t2 in
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
   let discriminator =
@@ -1029,7 +1034,7 @@ let onEquality with_evars tac (c,lbindc) =
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
   let eqn = EConstr.Unsafe.to_constr eqn in
-  let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
+  let (eq,u,eq_args) = find_this_eq_data_decompose gl (EConstr.of_constr eqn) in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
@@ -1041,7 +1046,7 @@ let onNegatedEquality with_evars tac =
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with
-    | Prod (_,t,u) when is_empty_type sigma u ->
+    | Prod (_,t,u) when is_empty_type sigma (EConstr.of_constr u) ->
         tclTHEN introf
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
@@ -1320,6 +1325,7 @@ let inject_if_homogenous_dependent_pair ty =
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
+    let t = EConstr.Unsafe.to_constr t in
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
@@ -1327,8 +1333,8 @@ let inject_if_homogenous_dependent_pair ty =
     (* check whether the equality deals with dep pairs or not *)
     let eqTypeDest = fst (decompose_app t) in
     if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
-    let hd1,ar1 = decompose_app_vect sigma (EConstr.of_constr t1) and
-        hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr t2) in
+    let hd1,ar1 = decompose_app_vect sigma t1 and
+        hd2,ar2 = decompose_app_vect sigma t2 in
     if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
     if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
     let ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr ar1.(0)) with Not_found -> raise Exit in
@@ -1369,6 +1375,9 @@ let simplify_args env sigma t =
     | _ -> t
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
+  let t = EConstr.Unsafe.to_constr t in
+  let t1 = EConstr.Unsafe.to_constr t1 in
+  let t2 = EConstr.Unsafe.to_constr t2 in
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (LocalAssum (e,t)) env in
   let evdref = ref sigma in
@@ -1396,7 +1405,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     (Tacticals.New.tclTHENFIRST
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
-           [inject_if_homogenous_dependent_pair ty;
+           [inject_if_homogenous_dependent_pair (EConstr.of_constr ty);
             Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
@@ -1536,7 +1545,12 @@ let decomp_tuple_term env sigma c t =
   let rec decomprec inner_code ex exty =
     let iterated_decomp =
     try
-      let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose ex in
+      let ex = EConstr.of_constr ex in
+      let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
+      let a = EConstr.Unsafe.to_constr a in
+      let p = EConstr.Unsafe.to_constr p in
+      let car = EConstr.Unsafe.to_constr car in
+      let cdr = EConstr.Unsafe.to_constr cdr in
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
       let cdrtyp = beta_applist sigma (EConstr.of_constr p,[EConstr.of_constr car]) in
@@ -1547,6 +1561,8 @@ let decomp_tuple_term env sigma c t =
   in decomprec (mkRel 1) c t
 
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
+  let dep_pair1 = EConstr.Unsafe.to_constr dep_pair1 in
+  let dep_pair2 = EConstr.Unsafe.to_constr dep_pair2 in
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in
   (* We find all possible decompositions *)
@@ -1583,7 +1599,7 @@ let cutSubstInConcl l2r eqn =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
+  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl (EConstr.of_constr eqn) in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
@@ -1602,7 +1618,7 @@ let cutSubstInHyp l2r eqn id =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
+  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl (EConstr.of_constr eqn) in
   let typ = pf_get_hyp_typ id gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
@@ -1682,20 +1698,21 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
     not (is_global glob_identity eq) 
   then raise Constr_matching.PatternMatchingFailure
 
-exception FoundHyp of (Id.t * constr * bool)
+exception FoundHyp of (Id.t * EConstr.constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
 let is_eq_x gl x d =
   let id = NamedDecl.get_id d in
   try
-    let is_var id c = match kind_of_term c with
+    let is_var id c = match EConstr.kind (project gl) c with
     | Var id' -> Id.equal id id'
     | _ -> false
     in
     let c = pf_nf_evar gl (NamedDecl.get_type d) in
+    let c = EConstr.of_constr c in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (is_var x lhs) && not (local_occur_var (project gl) x (EConstr.of_constr rhs)) then raise (FoundHyp (id,rhs,true));
-    if (is_var x rhs) && not (local_occur_var (project gl) x (EConstr.of_constr lhs)) then raise (FoundHyp (id,lhs,false))
+    if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
+    if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
     ()
 
@@ -1753,7 +1770,7 @@ let subst_one_var dep_proof_ok x =
           user_err ~hdr:"Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
-        with FoundHyp res -> res in
+        with FoundHyp (id, c, b) -> (id, EConstr.Unsafe.to_constr c, b) in
       subst_one dep_proof_ok x res
   end }
 
@@ -1788,7 +1805,9 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let select_equation_name decl =
       try
-        let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
+        let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in
+        let x = EConstr.Unsafe.to_constr x in
+        let y = EConstr.Unsafe.to_constr y in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match kind_of_term x, kind_of_term y with
@@ -1812,7 +1831,10 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
+    let c = EConstr.of_constr c in
     let _,_,(_,x,y) = find_eq_data_decompose c in
+    let x = EConstr.Unsafe.to_constr x in
+    let y = EConstr.Unsafe.to_constr y in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if Term.eq_constr x y then Proofview.tclUNIT () else
       match kind_of_term x, kind_of_term y with
@@ -1838,7 +1860,10 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
     try
+      let c = EConstr.of_constr c in
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let x = EConstr.Unsafe.to_constr x in
+      let y = EConstr.Unsafe.to_constr y in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
@@ -1858,21 +1883,24 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
 let cond_eq_term_left c t gl =
   try
+    let t = EConstr.of_constr t in
     let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true else failwith "not convertible"
+    if pf_conv_x gl (EConstr.of_constr c) x then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
+    let t = EConstr.of_constr t in
     let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then false else failwith "not convertible"
+    if pf_conv_x gl (EConstr.of_constr c) x then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
+    let t = EConstr.of_constr t in
     let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true
-    else if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr y) then false
+    if pf_conv_x gl (EConstr.of_constr c) x then true
+    else if pf_conv_x gl (EConstr.of_constr c) y then false
     else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
-- 
cgit v1.2.3


From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 tactics/equality.ml | 63 ++++++++++++++++++++++++++++++-----------------------
 1 file changed, 36 insertions(+), 27 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index e1a8d2bdb1..80f83f19bf 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -186,8 +186,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
 let instantiate_lemma gl c ty l l2r concl =
   let c = EConstr.of_constr c in
   let sigma, ct = pf_type_of gl c in
-  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
-  let t = EConstr.of_constr t in
+  let ct = EConstr.of_constr ct in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
   let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
@@ -413,6 +413,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+  let elim = EConstr.of_constr elim in
   let tac =
       Proofview.tclEFFECTS effs <*>
       general_elim_clause with_evars frzevars tac cls c t l
@@ -562,6 +563,7 @@ let general_multi_rewrite with_evars l cl tac =
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
       let (c, sigma) = run_delayed env sigma f in
+      let c = Miscops.map_with_bindings EConstr.Unsafe.to_constr c in
       tclWITHHOLES with_evars
         (general_rewrite_clause l2r with_evars ?tac c cl) sigma
     end }
@@ -646,6 +648,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     Tacticals.New.pf_constr_of_global sym (fun sym ->
     Tacticals.New.pf_constr_of_global e (fun e ->
     let eq = applist (e, [t1;c1;c2]) in
+    let sym = EConstr.of_constr sym in
+    let eq = EConstr.of_constr eq in
     tclTHENLAST
       (replace_core clause l2r eq)
       (tclFIRST
@@ -948,7 +952,7 @@ let gen_absurdity id =
   let hyp_typ = EConstr.of_constr hyp_typ in
   if is_empty_type sigma hyp_typ
   then
-    simplest_elim (mkVar id)
+    simplest_elim (EConstr.mkVar id)
   else
     tclZEROMSG (str "Not the negation of an equality.")
   end }
@@ -996,6 +1000,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let t = EConstr.Unsafe.to_constr t in
   let t1 = EConstr.Unsafe.to_constr t1 in
   let t2 = EConstr.Unsafe.to_constr t2 in
+  let eqn = EConstr.Unsafe.to_constr eqn in
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
   let discriminator =
@@ -1004,6 +1009,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
+  let absurd_term = EConstr.of_constr absurd_term in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
@@ -1023,18 +1029,15 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let c = EConstr.of_constr c in
-  let lbindc = Miscops.map_bindings EConstr.of_constr lbindc in
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
-  let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
-  let t' = EConstr.of_constr t' in
+  let t = EConstr.of_constr t in
+  let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  let eqn = EConstr.Unsafe.to_constr eqn in
-  let (eq,u,eq_args) = find_this_eq_data_decompose gl (EConstr.of_constr eqn) in
+  let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
@@ -1049,14 +1052,14 @@ let onNegatedEquality with_evars tac =
     | Prod (_,t,u) when is_empty_type sigma (EConstr.of_constr u) ->
         tclTHEN introf
           (onLastHypId (fun id ->
-            onEquality with_evars tac (mkVar id,NoBindings)))
+            onEquality with_evars tac (EConstr.mkVar id,NoBindings)))
     | _ ->
         tclZEROMSG (str "Not a negated primitive equality.")
   end }
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
-  | Some id -> onEquality with_evars discrEq (mkVar id,NoBindings)
+  | Some id -> onEquality with_evars discrEq (EConstr.mkVar id,NoBindings)
 
 let discr with_evars = onEquality with_evars discrEq
 
@@ -1070,7 +1073,7 @@ let discrEverywhere with_evars =
       (tclTHEN
 	(tclREPEAT introf)
 	(tryAllHyps
-          (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
+          (fun id -> tclCOMPLETE (discr with_evars (EConstr.mkVar id,NoBindings)))))
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
 (*    (fun gls ->
@@ -1194,17 +1197,15 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	| (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
       let ev = Evarutil.e_new_evar env evdref (EConstr.of_constr a) in
-      let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[EConstr.of_constr ev]) in
+      let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
-      match
-        Evd.existential_opt_value !evdref
-          (destEvar ev)
-      with
+      let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
+      match evopt with
 	| Some w ->
-            let w_type = unsafe_type_of env sigma (EConstr.of_constr w) in
+            let w_type = unsafe_type_of env !evdref w in
             if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
-              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+              applist(exist_term,[a;p_i_minus_1;EConstr.Unsafe.to_constr w;tuple_tail])
             else
               error "Cannot solve a unification problem."
 	| None ->
@@ -1354,7 +1355,8 @@ let inject_if_homogenous_dependent_pair ty =
       [Proofview.tclEFFECTS eff;
        intro;
        onLastHyp (fun hyp ->
-        tclTHENS (cut (mkApp (ceq,new_eq_args)))
+       let hyp = EConstr.Unsafe.to_constr hyp in
+        tclTHENS (cut (EConstr.of_constr (mkApp (ceq,new_eq_args))))
           [clear [destVar hyp];
            Proofview.V82.tactic (Tacmach.refine
              (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
@@ -1404,7 +1406,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Tacticals.New.tclTHENFIRST
       (Proofview.tclIGNORE (Proofview.Monad.List.map
-         (fun (pf,ty) -> tclTHENS (cut ty)
+         (fun (pf,ty) -> tclTHENS (cut (EConstr.of_constr ty))
            [inject_if_homogenous_dependent_pair (EConstr.of_constr ty);
             Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
          (if l2r then List.rev injectors else injectors)))
@@ -1452,6 +1454,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
         let destopt = match kind_of_term c with
         | Var id -> get_previous_hyp_position id gl
         | _ -> MoveLast in
+        let c = EConstr.of_constr c in
         let clear_tac =
           tclTRY (apply_clear_request clear_flag dft_clear_flag c) in
         (* Try should be removal if dependency were treated *)
@@ -1497,12 +1500,11 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
+    let c = EConstr.of_constr c in
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decomp_eq tac data (c, t) =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let c = EConstr.of_constr c in
-    let t = EConstr.of_constr t in
     let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
     decompEqThen (fun _ -> tac) data cl
   end }
@@ -1596,13 +1598,16 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
+  let eqn = EConstr.of_constr eqn in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl (EConstr.of_constr eqn) in
+  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
+  let typ = EConstr.of_constr typ in
+  let expected = EConstr.of_constr expected in
   let tac =
   tclTHENFIRST
     (tclTHENLIST [
@@ -1615,13 +1620,16 @@ let cutSubstInConcl l2r eqn =
   end }
 
 let cutSubstInHyp l2r eqn id =
+  let eqn = EConstr.of_constr eqn in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl (EConstr.of_constr eqn) in
+  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
+  let typ = EConstr.of_constr typ in
+  let expected = EConstr.of_constr expected in
   let tac =
     tclTHENFIRST
     (tclTHENLIST [
@@ -1653,8 +1661,9 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls =
+  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
-  let eq = pf_apply get_type_of gl (EConstr.of_constr c) in
+  let eq = pf_apply get_type_of gl c in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
@@ -1937,7 +1946,7 @@ let replace_term dir_opt c  =
 (* Declare rewriting tactic for intro patterns "<-" and "->" *)
 
 let _ =
-  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in
+  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars (Miscops.map_with_bindings EConstr.Unsafe.to_constr tac) c in
   Hook.set Tactics.general_rewrite_clause gmr
 
 let _ = Hook.set Tactics.subst_one subst_one
-- 
cgit v1.2.3


From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Nov 2016 20:35:01 +0100
Subject: Equality API using EConstr.

---
 tactics/equality.ml | 304 ++++++++++++++++++++++++++--------------------------
 1 file changed, 154 insertions(+), 150 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 80f83f19bf..4c79a61999 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -12,8 +12,9 @@ open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
+open EConstr
+open Vars
 open Namegen
 open Inductive
 open Inductiveops
@@ -46,6 +47,10 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
+let nlocal_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  NamedDecl.LocalAssum (na, inj t)
+
 (* Options *)
 
 let discriminate_introduction = ref true
@@ -144,7 +149,7 @@ let freeze_initial_evars sigma flags clause =
   (* We take evars of the type: this may include old evars! For excluding *)
   (* all old evars, including the ones occurring in the rewriting lemma, *)
   (* we would have to take the clenv_value *)
-  let newevars = Evd.evars_of_term (EConstr.Unsafe.to_constr (clenv_type clause)) in
+  let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in
   let evars =
     fold_undefined (fun evk _ evars ->
       if Evar.Set.mem evk newevars then evars
@@ -165,11 +170,9 @@ let side_tac tac sidetac =
 
 let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let env = Proofview.Goal.env gl in
-  let c = EConstr.of_constr c in
-  let ty = EConstr.of_constr ty in
-  let l = Miscops.map_bindings EConstr.of_constr l in
+  let sigma = project gl in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
-  let (equiv, args) = decompose_appvect (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+  let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
   let arglen = Array.length args in
   let () = if arglen < 2 then error "The term provided is not an applied relation." in
   let c1 = args.(arglen - 2) in
@@ -184,11 +187,9 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let c = EConstr.of_constr c in
   let sigma, ct = pf_type_of gl c in
   let ct = EConstr.of_constr ct in
   let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
-  let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -332,9 +333,9 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
 let jmeq_same_dom gl = function
   | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
   | Some t ->
-    let rels, t = decompose_prod_assum t in
+    let rels, t = decompose_prod_assum (project gl) t in
     let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
-    match EConstr.decompose_app (project gl) (EConstr.of_constr t) with
+    match decompose_app (project gl) t with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
 
@@ -342,6 +343,8 @@ let jmeq_same_dom gl = function
    eliminate lbeq on sort_of_gl. *)
 
 let find_elim hdcncl lft2rgt dep cls ot gl =
+  let sigma = project gl in
+  let is_global gr c = Termops.is_global sigma gr c in
   let inccl = Option.is_empty cls in
   if (is_global Coqlib.glob_eq hdcncl ||
       (is_global Coqlib.glob_jmeq hdcncl &&
@@ -349,7 +352,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     || Flags.version_less_or_equal Flags.V8_2
   then
     let c = 
-      match kind_of_term hdcncl with 
+      match EConstr.kind sigma hdcncl with 
       | Ind (ind_sp,u) -> 
 	let pr1 = 
 	  lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) 
@@ -377,6 +380,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	assert false
     in
       let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let elim = EConstr.of_constr elim in
       Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
   else
   let scheme_name = match dep, lft2rgt, inccl with
@@ -391,13 +395,14 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     | true, _, true -> rew_r2l_dep_scheme_kind
     | true, _, false -> rew_r2l_forward_dep_scheme_kind
   in
-  match kind_of_term hdcncl with
+  match EConstr.kind sigma hdcncl with
   | Ind (ind,u) -> 
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
       let Sigma (elim, sigma, p) =
 	Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
       in
+      let elim = EConstr.of_constr elim in
       Sigma ((elim, eff), sigma, p)
   | _ -> assert false
 
@@ -408,12 +413,12 @@ let type_of_clause cls gl = match cls with
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-  let isatomic = isProd (whd_zeta evd (EConstr.of_constr hdcncl)) in
+  let isatomic = isProd evd (EConstr.of_constr (whd_zeta evd hdcncl)) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
-  let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
+  let type_of_cls = EConstr.of_constr type_of_cls in
+  let dep = dep_proof_ok && dep_fun evd c type_of_cls in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-  let elim = EConstr.of_constr elim in
   let tac =
       Proofview.tclEFFECTS effs <*>
       general_elim_clause with_evars frzevars tac cls c t l
@@ -447,11 +452,11 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     Proofview.Goal.enter { enter = begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
-    let ctype = get_type_of env sigma (EConstr.of_constr c) in
-    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in
-      match match_with_equality_type sigma (EConstr.of_constr t) with
+    let ctype = get_type_of env sigma c in
+    let ctype = EConstr.of_constr ctype in
+    let rels, t = decompose_prod_assum sigma (EConstr.of_constr (whd_betaiotazeta sigma ctype)) in
+      match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
-          let hdcncl = EConstr.Unsafe.to_constr hdcncl in
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
 	    l with_evars frzevars dep_proof_ok hdcncl
@@ -465,10 +470,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
               | (e, info) ->
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
-	          let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *)
-	          match match_with_equality_type sigma (EConstr.of_constr t') with
+	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+	          let t' = EConstr.of_constr t' in
+	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
-                  let hdcncl = EConstr.Unsafe.to_constr hdcncl in
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
 		    (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
@@ -533,7 +538,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	let do_hyps =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids gl =
-	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
+	    let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
             let ids_of_hyps = pf_ids_of_hyps gl in
 	    Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
 	  in
@@ -563,7 +568,6 @@ let general_multi_rewrite with_evars l cl tac =
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
       let (c, sigma) = run_delayed env sigma f in
-      let c = Miscops.map_with_bindings EConstr.Unsafe.to_constr c in
       tclWITHHOLES with_evars
         (general_rewrite_clause l2r with_evars ?tac c cl) sigma
     end }
@@ -631,12 +635,14 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
   let get_type_of = pf_apply get_type_of gl in
-  let t1 = get_type_of (EConstr.of_constr c1)
-  and t2 = get_type_of (EConstr.of_constr c2) in
+  let t1 = get_type_of c1
+  and t2 = get_type_of c2 in
+  let t1 = EConstr.of_constr t1 in
+  let t2 = EConstr.of_constr t2 in
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) (EConstr.of_constr t1) (EConstr.of_constr t2) (Tacmach.New.project gl))
+      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -647,9 +653,9 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     let sym = build_coq_eq_sym () in
     Tacticals.New.pf_constr_of_global sym (fun sym ->
     Tacticals.New.pf_constr_of_global e (fun e ->
+    let e = EConstr.of_constr e in
     let eq = applist (e, [t1;c1;c2]) in
     let sym = EConstr.of_constr sym in
-    let eq = EConstr.of_constr eq in
     tclTHENLAST
       (replace_core clause l2r eq)
       (tclFIRST
@@ -727,12 +733,10 @@ let _ =
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
 let find_positions env sigma t1 t2 =
-  let open EConstr in
   let project env sorts posn t1 t2 =
-    let t1 = EConstr.Unsafe.to_constr t1 in
-    let t2 = EConstr.Unsafe.to_constr t2 in
-    let ty1 = get_type_of env sigma (EConstr.of_constr t1) in
-    let s = get_sort_family_of env sigma (EConstr.of_constr ty1) in
+    let ty1 = get_type_of env sigma t1 in
+    let ty1 = EConstr.of_constr ty1 in
+    let s = get_sort_family_of env sigma ty1 in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
   in
@@ -854,7 +858,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma (EConstr.of_constr head)))
+    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -871,12 +875,12 @@ let descend_then env sigma head dirn =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
+	it_mkLambda_or_LetIn result (name_context env cstr.(i-1).cs_args) in
       let brl =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      EConstr.Unsafe.to_constr (Inductiveops.make_case_or_project env sigma indf ci (EConstr.of_constr p) (EConstr.of_constr head) (Array.map_of_list EConstr.of_constr brl))))
+      Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -897,7 +901,7 @@ let descend_then env sigma head dirn =
 
 let build_selector env sigma dirn c ind special default =
   let IndType(indf,_) =
-    try find_rectype env sigma (EConstr.of_constr ind)
+    try find_rectype env sigma ind
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors
           like T := c : (A:Set)A->T and a discrimination
@@ -909,7 +913,8 @@ let build_selector env sigma dirn c ind special default =
 		 dependent types.") in
   let (indp,_) = dest_ind_family indf in
   let ind, _ = check_privacy env indp in
-  let typ = Retyping.get_type_of env sigma (EConstr.of_constr default) in
+  let typ = Retyping.get_type_of env sigma default in
+  let typ = EConstr.of_constr typ in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
@@ -922,9 +927,14 @@ let build_selector env sigma dirn c ind special default =
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
 
+let build_coq_False () = EConstr.of_constr (build_coq_False ())
+let build_coq_True () = EConstr.of_constr (build_coq_True ())
+let build_coq_I () = EConstr.of_constr (build_coq_I ())
+
 let rec build_discriminator env sigma dirn c = function
   | [] ->
-      let ind = get_type_of env sigma (EConstr.of_constr c) in
+      let ind = get_type_of env sigma c in
+      let ind = EConstr.of_constr ind in
       let true_0,false_0 =
         build_coq_True(),build_coq_False() in
       build_selector env sigma dirn c ind true_0 false_0
@@ -952,7 +962,7 @@ let gen_absurdity id =
   let hyp_typ = EConstr.of_constr hyp_typ in
   if is_empty_type sigma hyp_typ
   then
-    simplest_elim (EConstr.mkVar id)
+    simplest_elim (mkVar id)
   else
     tclZEROMSG (str "Not the negation of an equality.")
   end }
@@ -980,6 +990,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
   let absurd_term  = build_coq_False () in
   let eq_elim, eff = ind_scheme_of_eq lbeq in
   let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
+  let eq_elim = EConstr.of_constr eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
     eff
 
@@ -987,8 +998,6 @@ let eq_baseid = Id.of_string "e"
 
 let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
-  let f = EConstr.of_constr f in
-  let t = EConstr.of_constr t in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
     (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
@@ -997,19 +1006,14 @@ let apply_on_clause (f,t) clause =
   clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
-  let t = EConstr.Unsafe.to_constr t in
-  let t1 = EConstr.Unsafe.to_constr t1 in
-  let t2 = EConstr.Unsafe.to_constr t2 in
-  let eqn = EConstr.Unsafe.to_constr eqn in
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
+  let e_env = push_named (nlocal_assum (e, t)) env in
   let discriminator =
     build_discriminator e_env sigma dirn (mkVar e) cpath in
   let sigma,(pf, absurd_term), eff = 
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
-  let absurd_term = EConstr.of_constr absurd_term in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
@@ -1047,19 +1051,20 @@ let onNegatedEquality with_evars tac =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
+    let ccl = EConstr.of_constr ccl in
     let env = Proofview.Goal.env gl in
-    match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with
-    | Prod (_,t,u) when is_empty_type sigma (EConstr.of_constr u) ->
+    match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with
+    | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
-            onEquality with_evars tac (EConstr.mkVar id,NoBindings)))
+            onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
         tclZEROMSG (str "Not a negated primitive equality.")
   end }
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
-  | Some id -> onEquality with_evars discrEq (EConstr.mkVar id,NoBindings)
+  | Some id -> onEquality with_evars discrEq (mkVar id,NoBindings)
 
 let discr with_evars = onEquality with_evars discrEq
 
@@ -1073,7 +1078,7 @@ let discrEverywhere with_evars =
       (tclTHEN
 	(tclREPEAT introf)
 	(tryAllHyps
-          (fun id -> tclCOMPLETE (discr with_evars (EConstr.mkVar id,NoBindings)))))
+          (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
 (*    (fun gls ->
@@ -1103,9 +1108,10 @@ let find_sigma_data env s = build_sigma_type ()
  *)
 
 let make_tuple env sigma (rterm,rty) lind =
-  assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
-  let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
-  let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in
+  assert (not (noccurn sigma lind rty));
+  let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
+  let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+  let a = EConstr.of_constr a in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1113,6 +1119,8 @@ let make_tuple env sigma (rterm,rty) lind =
   let p = mkLambda (na, a, rty) in
   let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
   let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
+  let exist_term = EConstr.of_constr exist_term in
+  let sig_term = EConstr.of_constr sig_term in
     sigma,
     (applist(exist_term,[a;p;(mkRel lind);rterm]),
      applist(sig_term,[a;p]))
@@ -1125,9 +1133,10 @@ let make_tuple env sigma (rterm,rty) lind =
    normalization *)
 
 let minimal_free_rels env sigma (c,cty) =
-  let cty_rels = free_rels sigma (EConstr.of_constr cty) in
-  let cty' = simpl env sigma (EConstr.of_constr cty) in
-  let rels' = free_rels sigma (EConstr.of_constr cty') in
+  let cty_rels = free_rels sigma cty in
+  let cty' = simpl env sigma cty in
+  let cty' = EConstr.of_constr cty' in
+  let rels' = free_rels sigma cty' in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
   else
@@ -1139,7 +1148,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, EConstr.of_constr (unsafe_type_of env sigma (mkRel i))))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1185,27 +1194,30 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in
+      let dflt_typ = unsafe_type_of env sigma dflt in
       try
-	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
+	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) p_i !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
 	error "Cannot solve a unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with
-	| (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p)
+      let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+	| (_sigS,[a;p]) -> (a, p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
-      let ev = Evarutil.e_new_evar env evdref (EConstr.of_constr a) in
-      let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[ev]) in
+      let ev = Evarutil.e_new_evar env evdref a in
+      let rty = beta_applist sigma (p_i_minus_1,[ev]) in
+      let rty = EConstr.of_constr rty in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
       match evopt with
 	| Some w ->
             let w_type = unsafe_type_of env !evdref w in
-            if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
+            let w_type = EConstr.of_constr w_type in
+            if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
-              applist(exist_term,[a;p_i_minus_1;EConstr.Unsafe.to_constr w;tuple_tail])
+	      let exist_term = EConstr.of_constr exist_term in
+              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
 	| None ->
@@ -1218,7 +1230,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
-    !evdref, Evarutil.nf_evar !evdref scf
+    !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf))
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
@@ -1280,18 +1292,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
-  let sort_of_zty = get_sort_of env sigma (EConstr.of_constr zty) in
+  let sort_of_zty = get_sort_of env sigma zty in
   let sorted_rels = Int.Set.elements rels in
   let sigma, (tuple,tuplety) =
     List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels
   in
-  assert (closed0 tuplety);
+  assert (closed0 sigma tuplety);
   let n = List.length sorted_rels in
   let sigma, dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c))
+  | [] -> make_iterated_tuple env sigma dflt (c,EConstr.of_constr (unsafe_type_of env sigma c))
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1326,40 +1338,44 @@ let inject_if_homogenous_dependent_pair ty =
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
-    let t = EConstr.Unsafe.to_constr t in
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
+    let ceq = EConstr.of_constr ceq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
     let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
     (* check whether the equality deals with dep pairs or not *)
-    let eqTypeDest = fst (decompose_app t) in
-    if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
+    let eqTypeDest = fst (decompose_app sigma t) in
+    if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit;
     let hd1,ar1 = decompose_app_vect sigma t1 and
         hd2,ar2 = decompose_app_vect sigma t2 in
-    if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
-    if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr ar1.(0)) with Not_found -> raise Exit in
+    let hd1 = EConstr.of_constr hd1 in
+    let hd2 = EConstr.of_constr hd2 in
+    let ar1 = Array.map EConstr.of_constr ar1 in
+    let ar2 = Array.map EConstr.of_constr ar2 in
+    if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
+    if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
+    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
-      pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit;
+      pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr ar1.(3));ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|EConstr.of_constr (pf_unsafe_type_of gl ar1.(3));ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+    let inj2 = EConstr.of_constr inj2 in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
        intro;
        onLastHyp (fun hyp ->
-       let hyp = EConstr.Unsafe.to_constr hyp in
-        tclTHENS (cut (EConstr.of_constr (mkApp (ceq,new_eq_args))))
-          [clear [destVar hyp];
+        tclTHENS (cut (mkApp (ceq,new_eq_args)))
+          [clear [destVar sigma hyp];
            Proofview.V82.tactic (Tacmach.refine
-             (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
+             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1371,17 +1387,15 @@ let inject_if_homogenous_dependent_pair ty =
 
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
-  match decompose_app t with
-    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma (EConstr.of_constr c1);simpl env sigma (EConstr.of_constr c2)])
-    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma (EConstr.of_constr c1);t2;simpl env sigma (EConstr.of_constr c2)])
+  let simpl env sigma c = EConstr.of_constr (simpl env sigma c) in
+  match decompose_app sigma t with
+    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
-  let t = EConstr.Unsafe.to_constr t in
-  let t1 = EConstr.Unsafe.to_constr t1 in
-  let t2 = EConstr.Unsafe.to_constr t2 in
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (LocalAssum (e,t)) env in
+  let e_env = push_named (nlocal_assum (e,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
@@ -1389,12 +1403,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
+      let congr = EConstr.of_constr congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
-      let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
+      let sigma, pf_typ = Typing.type_of env sigma pf in
+      let pf_typ = EConstr.of_constr pf_typ in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
-      let ty = simplify_args env sigma (EConstr.Unsafe.to_constr (clenv_type inj_clause)) in
-      let pf = EConstr.Unsafe.to_constr pf in
+      let ty = simplify_args env sigma (clenv_type inj_clause) in
 	evdref := sigma;
 	Some (pf, ty)
     with Failure _ -> None
@@ -1406,9 +1421,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Tacticals.New.tclTHENFIRST
       (Proofview.tclIGNORE (Proofview.Monad.List.map
-         (fun (pf,ty) -> tclTHENS (cut (EConstr.of_constr ty))
-           [inject_if_homogenous_dependent_pair (EConstr.of_constr ty);
-            Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
+         (fun (pf,ty) -> tclTHENS (cut ty)
+           [inject_if_homogenous_dependent_pair ty;
+            Proofview.V82.tactic (Tacmach.refine pf)])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
@@ -1428,7 +1443,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
      tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
-	(tac (EConstr.Unsafe.to_constr (clenv_value eq_clause)))
+	(tac (clenv_value eq_clause))
 
 let get_previous_hyp_position id gl =
   let rec aux dest = function
@@ -1451,10 +1466,10 @@ let injEq ?(old=false) with_evars clear_flag ipats =
     match ipats_style with
     | Some ipats ->
       Proofview.Goal.enter { enter = begin fun gl ->
-        let destopt = match kind_of_term c with
+        let sigma = project gl in
+        let destopt = match EConstr.kind sigma c with
         | Var id -> get_previous_hyp_position id gl
         | _ -> MoveLast in
-        let c = EConstr.of_constr c in
         let clear_tac =
           tclTRY (apply_clear_request clear_flag dft_clear_flag c) in
         (* Try should be removal if dependency were treated *)
@@ -1488,10 +1503,10 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-        ntac (EConstr.Unsafe.to_constr (clenv_value clause)) 0
+        ntac (clenv_value clause) 0
     | Inr posns ->
 	inject_at_positions env sigma true u clause posns
-          (ntac (EConstr.Unsafe.to_constr (clenv_value clause)))
+          (ntac (clenv_value clause))
   end }
 
 let dEqThen with_evars ntac = function
@@ -1500,7 +1515,6 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
-    let c = EConstr.of_constr c in
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decomp_eq tac data (c, t) =
@@ -1547,26 +1561,24 @@ let decomp_tuple_term env sigma c t =
   let rec decomprec inner_code ex exty =
     let iterated_decomp =
     try
-      let ex = EConstr.of_constr ex in
       let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
-      let a = EConstr.Unsafe.to_constr a in
-      let p = EConstr.Unsafe.to_constr p in
-      let car = EConstr.Unsafe.to_constr car in
-      let cdr = EConstr.Unsafe.to_constr cdr in
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
-      let cdrtyp = beta_applist sigma (EConstr.of_constr p,[EConstr.of_constr car]) in
+      let cdrtyp = beta_applist sigma (p,[car]) in
+      let cdrtyp = EConstr.of_constr cdrtyp in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
     in [((ex,exty),inner_code)]::iterated_decomp
   in decomprec (mkRel 1) c t
 
+let lambda_create env (a,b) =
+  mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b)
+
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
-  let dep_pair1 = EConstr.Unsafe.to_constr dep_pair1 in
-  let dep_pair2 = EConstr.Unsafe.to_constr dep_pair2 in
   let sigma = Sigma.to_evar_map sigma in
-  let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in
+  let typ = get_type_of env sigma dep_pair1 in
+  let typ = EConstr.of_constr typ in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
   let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
@@ -1581,15 +1593,18 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
-  let pred_body = beta_applist sigma (EConstr.of_constr abst_B, List.map EConstr.of_constr proj_list) in
+      (fun (e,t) body -> lambda_create env (t,EConstr.of_constr (subst_term sigma e body))) e1_list b in
+  let pred_body = beta_applist sigma (abst_B,proj_list) in
+  let pred_body = EConstr.of_constr pred_body in
   let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
-  let expected_goal = beta_applist sigma (EConstr.of_constr abst_B,List.map (fst %> EConstr.of_constr) e2_list) in
+  let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
-  let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
+  let expected_goal = EConstr.of_constr expected_goal in
+  let expected_goal = nf_betaiota sigma expected_goal in
+  let expected_goal = EConstr.of_constr expected_goal in
   (* Retype to get universes right *)
-  let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in
-  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in
+  let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
+  let sigma, _ = Typing.type_of env sigma body in
   Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
 
 (* Like "replace" but decompose dependent equalities                      *)
@@ -1598,16 +1613,14 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  let eqn = EConstr.of_constr eqn in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
+  let typ = EConstr.of_constr typ in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let typ = EConstr.of_constr typ in
-  let expected = EConstr.of_constr expected in
   let tac =
   tclTHENFIRST
     (tclTHENLIST [
@@ -1620,16 +1633,14 @@ let cutSubstInConcl l2r eqn =
   end }
 
 let cutSubstInHyp l2r eqn id =
-  let eqn = EConstr.of_constr eqn in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
+  let typ = EConstr.of_constr typ in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let typ = EConstr.of_constr typ in
-  let expected = EConstr.of_constr expected in
   let tac =
     tclTHENFIRST
     (tclTHENLIST [
@@ -1661,9 +1672,9 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls =
-  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
   let eq = pf_apply get_type_of gl c in
+  let eq = EConstr.of_constr eq in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
@@ -1707,7 +1718,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
     not (is_global glob_identity eq) 
   then raise Constr_matching.PatternMatchingFailure
 
-exception FoundHyp of (Id.t * EConstr.constr * bool)
+exception FoundHyp of (Id.t * constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
 let is_eq_x gl x d =
@@ -1779,7 +1790,7 @@ let subst_one_var dep_proof_ok x =
           user_err ~hdr:"Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
-        with FoundHyp (id, c, b) -> (id, EConstr.Unsafe.to_constr c, b) in
+        with FoundHyp res -> res in
       subst_one dep_proof_ok x res
   end }
 
@@ -1811,15 +1822,14 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
+    let sigma = project gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in
-        let x = EConstr.Unsafe.to_constr x in
-        let y = EConstr.Unsafe.to_constr y in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
-        match kind_of_term x, kind_of_term y with
+        match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
             Some (NamedDecl.get_id decl)
         | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
@@ -1842,14 +1852,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
     let c = EConstr.of_constr c in
     let _,_,(_,x,y) = find_eq_data_decompose c in
-    let x = EConstr.Unsafe.to_constr x in
-    let y = EConstr.Unsafe.to_constr y in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-    if Term.eq_constr x y then Proofview.tclUNIT () else
-      match kind_of_term x, kind_of_term y with
-      | Var x', _ when not (occur_term sigma (EConstr.of_constr x) (EConstr.of_constr y)) && not (is_evaluable env (EvalVarRef x')) ->
+    if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
+      match EConstr.kind sigma x, EConstr.kind sigma y with
+      | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (occur_term sigma (EConstr.of_constr y) (EConstr.of_constr x)) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
@@ -1866,19 +1874,18 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
     try
       let c = EConstr.of_constr c in
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
-      let x = EConstr.Unsafe.to_constr x in
-      let y = EConstr.Unsafe.to_constr y in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-      if Term.eq_constr x y then failwith "caught";
-      match kind_of_term x with Var x -> x | _ ->
-      match kind_of_term y with Var y -> y | _ -> failwith "caught"
+      if EConstr.eq_constr sigma x y then failwith "caught";
+      match EConstr.kind sigma x with Var x -> x | _ ->
+      match EConstr.kind sigma y with Var y -> y | _ -> failwith "caught"
     with Constr_matching.PatternMatchingFailure -> failwith "caught" in
   let test p = try Some (test p) with Failure _ -> None in
   let hyps = pf_hyps_types gl in
@@ -1892,24 +1899,21 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
 let cond_eq_term_left c t gl =
   try
-    let t = EConstr.of_constr t in
     let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) x then true else failwith "not convertible"
+    if pf_conv_x gl c x then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
-    let t = EConstr.of_constr t in
     let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) x then false else failwith "not convertible"
+    if pf_conv_x gl c x then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
-    let t = EConstr.of_constr t in
     let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) x then true
-    else if pf_conv_x gl (EConstr.of_constr c) y then false
+    if pf_conv_x gl c x then true
+    else if pf_conv_x gl c y then false
     else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
@@ -1920,7 +1924,7 @@ let rewrite_assumption_cond cond_eq_term cl =
         let id = NamedDecl.get_id hyp in
 	begin
 	  try
-            let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
+            let dir = cond_eq_term (EConstr.of_constr (NamedDecl.get_type hyp)) gl in
 	    general_rewrite_clause dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
@@ -1946,7 +1950,7 @@ let replace_term dir_opt c  =
 (* Declare rewriting tactic for intro patterns "<-" and "->" *)
 
 let _ =
-  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars (Miscops.map_with_bindings EConstr.Unsafe.to_constr tac) c in
+  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in
   Hook.set Tactics.general_rewrite_clause gmr
 
 let _ = Hook.set Tactics.subst_one subst_one
-- 
cgit v1.2.3


From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 20:09:26 +0100
Subject: Eliminating parts of the right-hand side compatibility layer

---
 tactics/equality.ml | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4c79a61999..2eead2d22b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -183,7 +183,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
     w_unify_to_subterm_all ~flags env eqclause.evd
-      (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr concl)
+      ((if l2r then c1 else c2),concl)
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
@@ -314,6 +314,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     | None -> pf_nf_concl gl
     | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
     in
+    let typ = EConstr.of_constr typ in
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
     else tclMAP try_clause cs
@@ -1207,7 +1208,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
       let ev = Evarutil.e_new_evar env evdref a in
       let rty = beta_applist sigma (p_i_minus_1,[ev]) in
-      let rty = EConstr.of_constr rty in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
       match evopt with
@@ -1348,10 +1348,6 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit;
     let hd1,ar1 = decompose_app_vect sigma t1 and
         hd2,ar2 = decompose_app_vect sigma t2 in
-    let hd1 = EConstr.of_constr hd1 in
-    let hd2 = EConstr.of_constr hd2 in
-    let ar1 = Array.map EConstr.of_constr ar1 in
-    let ar2 = Array.map EConstr.of_constr ar2 in
     if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
     if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
     let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
@@ -1565,7 +1561,6 @@ let decomp_tuple_term env sigma c t =
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
       let cdrtyp = beta_applist sigma (p,[car]) in
-      let cdrtyp = EConstr.of_constr cdrtyp in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
@@ -1593,13 +1588,11 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,EConstr.of_constr (subst_term sigma e body))) e1_list b in
+      (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in
   let pred_body = beta_applist sigma (abst_B,proj_list) in
-  let pred_body = EConstr.of_constr pred_body in
   let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
-  let expected_goal = EConstr.of_constr expected_goal in
   let expected_goal = nf_betaiota sigma expected_goal in
   let expected_goal = EConstr.of_constr expected_goal in
   (* Retype to get universes right *)
-- 
cgit v1.2.3


From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 22:16:08 +0100
Subject: Proofview.Goal primitive now return EConstrs.

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

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2eead2d22b..209c9eb662 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -312,9 +312,8 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     in
     let typ = match cls with
     | None -> pf_nf_concl gl
-    | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
+    | Some id -> EConstr.of_constr (pf_get_hyp_typ id (Proofview.Goal.assume gl))
     in
-    let typ = EConstr.of_constr typ in
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
     else tclMAP try_clause cs
@@ -409,7 +408,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 
 let type_of_clause cls gl = match cls with
   | None -> Proofview.Goal.concl gl
-  | Some id -> pf_get_hyp_typ id gl
+  | Some id -> EConstr.of_constr (pf_get_hyp_typ id gl)
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
@@ -417,7 +416,6 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let isatomic = isProd evd (EConstr.of_constr (whd_zeta evd hdcncl)) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
-  let type_of_cls = EConstr.of_constr type_of_cls in
   let dep = dep_proof_ok && dep_fun evd c type_of_cls in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
   let tac =
@@ -1052,7 +1050,6 @@ let onNegatedEquality with_evars tac =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
-    let ccl = EConstr.of_constr ccl in
     let env = Proofview.Goal.env gl in
     match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with
     | Prod (_,t,u) when is_empty_type sigma u ->
@@ -1611,7 +1608,6 @@ let cutSubstInConcl l2r eqn =
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
-  let typ = EConstr.of_constr typ in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
   let tac =
@@ -1752,7 +1748,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       hyps
       (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
-  let depconcl = occur_var env sigma x (EConstr.of_constr concl) in
+  let depconcl = occur_var env sigma x concl in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-- 
cgit v1.2.3


From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

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

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 209c9eb662..494f36d7d9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -413,7 +413,7 @@ let type_of_clause cls gl = match cls with
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-  let isatomic = isProd evd (EConstr.of_constr (whd_zeta evd hdcncl)) in
+  let isatomic = isProd evd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd c type_of_cls in
@@ -453,7 +453,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
     let ctype = EConstr.of_constr ctype in
-    let rels, t = decompose_prod_assum sigma (EConstr.of_constr (whd_betaiotazeta sigma ctype)) in
+    let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -470,7 +470,6 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
-	          let t' = EConstr.of_constr t' in
 	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -1051,7 +1050,7 @@ let onNegatedEquality with_evars tac =
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with
+    match EConstr.kind sigma (hnf_constr env sigma ccl) with
     | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
@@ -1133,7 +1132,6 @@ let make_tuple env sigma (rterm,rty) lind =
 let minimal_free_rels env sigma (c,cty) =
   let cty_rels = free_rels sigma cty in
   let cty' = simpl env sigma cty in
-  let cty' = EConstr.of_constr cty' in
   let rels' = free_rels sigma cty' in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
@@ -1380,7 +1378,6 @@ let inject_if_homogenous_dependent_pair ty =
 
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
-  let simpl env sigma c = EConstr.of_constr (simpl env sigma c) in
   match decompose_app sigma t with
     | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
@@ -1591,7 +1588,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
-  let expected_goal = EConstr.of_constr expected_goal in
   (* Retype to get universes right *)
   let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
-- 
cgit v1.2.3


From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 17:15:15 +0100
Subject: Removing compatibility layers in Retyping

---
 tactics/equality.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 494f36d7d9..e1c39bb34e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -188,7 +188,6 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
 
 let instantiate_lemma gl c ty l l2r concl =
   let sigma, ct = pf_type_of gl c in
-  let ct = EConstr.of_constr ct in
   let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
@@ -452,7 +451,6 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
-    let ctype = EConstr.of_constr ctype in
     let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
@@ -635,8 +633,6 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let get_type_of = pf_apply get_type_of gl in
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
-  let t1 = EConstr.of_constr t1 in
-  let t2 = EConstr.of_constr t2 in
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
@@ -733,7 +729,6 @@ let _ =
 let find_positions env sigma t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
-    let ty1 = EConstr.of_constr ty1 in
     let s = get_sort_family_of env sigma ty1 in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
@@ -856,7 +851,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
+    try find_rectype env sigma (get_type_of env sigma head)
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -912,7 +907,6 @@ let build_selector env sigma dirn c ind special default =
   let (indp,_) = dest_ind_family indf in
   let ind, _ = check_privacy env indp in
   let typ = Retyping.get_type_of env sigma default in
-  let typ = EConstr.of_constr typ in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
@@ -932,7 +926,6 @@ let build_coq_I () = EConstr.of_constr (build_coq_I ())
 let rec build_discriminator env sigma dirn c = function
   | [] ->
       let ind = get_type_of env sigma c in
-      let ind = EConstr.of_constr ind in
       let true_0,false_0 =
         build_coq_True(),build_coq_False() in
       build_selector env sigma dirn c ind true_0 false_0
@@ -1108,7 +1101,6 @@ let make_tuple env sigma (rterm,rty) lind =
   assert (not (noccurn sigma lind rty));
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
-  let a = EConstr.of_constr a in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1396,7 +1388,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let congr = EConstr.of_constr congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
       let sigma, pf_typ = Typing.type_of env sigma pf in
-      let pf_typ = EConstr.of_constr pf_typ in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1567,7 +1558,6 @@ let lambda_create env (a,b) =
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
-  let typ = EConstr.of_constr typ in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
   let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
@@ -1659,7 +1649,6 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 let substClause l2r c cls =
   Proofview.Goal.enter { enter = begin fun gl ->
   let eq = pf_apply get_type_of gl c in
-  let eq = EConstr.of_constr eq in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
-- 
cgit v1.2.3


From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 tactics/equality.ml | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index e1c39bb34e..7dcfd419e7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -311,7 +311,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     in
     let typ = match cls with
     | None -> pf_nf_concl gl
-    | Some id -> EConstr.of_constr (pf_get_hyp_typ id (Proofview.Goal.assume gl))
+    | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
     in
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
@@ -407,7 +407,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 
 let type_of_clause cls gl = match cls with
   | None -> Proofview.Goal.concl gl
-  | Some id -> EConstr.of_constr (pf_get_hyp_typ id gl)
+  | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
@@ -950,7 +950,6 @@ let gen_absurdity id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
-  let hyp_typ = EConstr.of_constr hyp_typ in
   if is_empty_type sigma hyp_typ
   then
     simplest_elim (mkVar id)
@@ -1027,7 +1026,6 @@ let onEquality with_evars tac (c,lbindc) =
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
-  let t = EConstr.of_constr t in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
@@ -1136,7 +1134,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, EConstr.of_constr (unsafe_type_of env sigma (mkRel i))))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1184,7 +1182,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       (* is the default value typable with the expected type *)
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
-	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) p_i !evdref in
+	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
@@ -1200,7 +1198,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       match evopt with
 	| Some w ->
             let w_type = unsafe_type_of env !evdref w in
-            let w_type = EConstr.of_constr w_type in
             if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
 	      let exist_term = EConstr.of_constr exist_term in
@@ -1290,7 +1287,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,EConstr.of_constr (unsafe_type_of env sigma c))
+  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1345,7 +1342,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|EConstr.of_constr (pf_unsafe_type_of gl ar1.(3));ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let inj2 = EConstr.of_constr inj2 in
@@ -1613,7 +1610,6 @@ let cutSubstInHyp l2r eqn id =
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
-  let typ = EConstr.of_constr typ in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
   let tac =
@@ -1702,8 +1698,7 @@ let is_eq_x gl x d =
     | Var id' -> Id.equal id id'
     | _ -> false
     in
-    let c = pf_nf_evar gl (NamedDecl.get_type d) in
-    let c = EConstr.of_constr c in
+    let c = pf_nf_evar gl (EConstr.of_constr (NamedDecl.get_type d)) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
     if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
     if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1852,7 +1847,6 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
     try
-      let c = EConstr.of_constr c in
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
-- 
cgit v1.2.3


From 01849481fbabc3a3fa6c483e703996b01e37fca5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 01:25:11 +0100
Subject: Removing compatibility layers from Tacticals

---
 tactics/equality.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7dcfd419e7..c80cf4416c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -647,9 +647,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     let sym = build_coq_eq_sym () in
     Tacticals.New.pf_constr_of_global sym (fun sym ->
     Tacticals.New.pf_constr_of_global e (fun e ->
-    let e = EConstr.of_constr e in
     let eq = applist (e, [t1;c1;c2]) in
-    let sym = EConstr.of_constr sym in
     tclTHENLAST
       (replace_core clause l2r eq)
       (tclFIRST
-- 
cgit v1.2.3


From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index c80cf4416c..072da995db 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1212,7 +1212,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
-    !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf))
+    !evdref, Evarutil.nf_evar !evdref scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
-- 
cgit v1.2.3


From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
---
 tactics/equality.ml | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 072da995db..122b64777e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -13,12 +13,12 @@ open Names
 open Nameops
 open Term
 open Termops
+open Environ
 open EConstr
 open Vars
 open Namegen
 open Inductive
 open Inductiveops
-open Environ
 open Libnames
 open Globnames
 open Reductionops
@@ -47,10 +47,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-let nlocal_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  NamedDecl.LocalAssum (na, inj t)
-
 (* Options *)
 
 let discriminate_introduction = ref true
@@ -333,7 +329,7 @@ let jmeq_same_dom gl = function
   | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
   | Some t ->
     let rels, t = decompose_prod_assum (project gl) t in
-    let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
+    let env = push_rel_context rels (Proofview.Goal.env gl) in
     match decompose_app (project gl) t with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
@@ -857,16 +853,19 @@ let descend_then env sigma head dirn =
   let (mib,mip) = lookup_mind_specif env ind in
   let cstr = get_constructors env indf in
   let dirn_nlams = cstr.(dirn-1).cs_nargs in
-  let dirn_env = push_rel_context cstr.(dirn-1).cs_args env in
+  let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
       let deparsign = make_arity_signature env true indf in
+      let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	it_mkLambda_or_LetIn result (name_context env cstr.(i-1).cs_args) in
+	let args = name_context env cstr.(i-1).cs_args in
+	let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in
+	it_mkLambda_or_LetIn result args in
       let brl =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
@@ -907,11 +906,13 @@ let build_selector env sigma dirn c ind special default =
   let typ = Retyping.get_type_of env sigma default in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
+  let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
   let p = it_mkLambda_or_LetIn typ deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
     let endpt = if Int.equal i dirn then special else default in
-    it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
+    let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstrs.(i-1).cs_args in
+    it_mkLambda_or_LetIn endpt args in
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
@@ -995,7 +996,7 @@ let apply_on_clause (f,t) clause =
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (nlocal_assum (e, t)) env in
+  let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
   let discriminator =
     build_discriminator e_env sigma dirn (mkVar e) cpath in
   let sigma,(pf, absurd_term), eff = 
@@ -1372,7 +1373,7 @@ let simplify_args env sigma t =
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (nlocal_assum (e,t)) env in
+  let e_env = push_named (LocalAssum (e,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
@@ -1696,7 +1697,7 @@ let is_eq_x gl x d =
     | Var id' -> Id.equal id id'
     | _ -> false
     in
-    let c = pf_nf_evar gl (EConstr.of_constr (NamedDecl.get_type d)) in
+    let c = pf_nf_evar gl (NamedDecl.get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
     if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
     if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1793,7 +1794,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let select_equation_name decl =
       try
-        let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in
+        let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
@@ -1817,7 +1818,6 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
-    let c = EConstr.of_constr c in
     let _,_,(_,x,y) = find_eq_data_decompose c in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
@@ -1890,7 +1890,7 @@ let rewrite_assumption_cond cond_eq_term cl =
         let id = NamedDecl.get_id hyp in
 	begin
 	  try
-            let dir = cond_eq_term (EConstr.of_constr (NamedDecl.get_type hyp)) gl in
+            let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
 	    general_rewrite_clause dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
-- 
cgit v1.2.3


From 390fd4ac0a969103caeb5db3e5138e26f9a533de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 17:49:11 +0100
Subject: Chasing a few unsafe constr coercions.

---
 tactics/equality.ml | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 122b64777e..7f7a07b8fe 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1300,19 +1300,6 @@ let build_injector env sigma dflt c cpath =
   let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in
     sigma, (injcode,resty)
 
-(*
-let try_delta_expand env sigma t =
-  let whdt = whd_all env sigma t  in
-  let rec hd_rec c  =
-    match kind_of_term c with
-      | Construct _ -> whdt
-      | App (f,_)  -> hd_rec f
-      | Cast (c,_,_) -> hd_rec c
-      | _  -> t
-  in
-  hd_rec whdt
-*)
-
 let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
-- 
cgit v1.2.3


From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
---
 tactics/equality.ml | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7f7a07b8fe..d9b6685179 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -857,14 +857,13 @@ let descend_then env sigma head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let deparsign = make_arity_signature env true indf in
-      let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
+      let deparsign = make_arity_signature env sigma true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	let args = name_context env cstr.(i-1).cs_args in
-	let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in
+	let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in
+	let args = name_context env sigma cs_args in
 	it_mkLambda_or_LetIn result args in
       let brl =
         List.map build_branch
@@ -905,8 +904,7 @@ let build_selector env sigma dirn c ind special default =
   let ind, _ = check_privacy env indp in
   let typ = Retyping.get_type_of env sigma default in
   let (mib,mip) = lookup_mind_specif env ind in
-  let deparsign = make_arity_signature env true indf in
-  let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
+  let deparsign = make_arity_signature env sigma true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
@@ -1535,9 +1533,6 @@ let decomp_tuple_term env sigma c t =
     in [((ex,exty),inner_code)]::iterated_decomp
   in decomprec (mkRel 1) c t
 
-let lambda_create env (a,b) =
-  mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b)
-
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
@@ -1555,9 +1550,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in
+      (fun (e,t) body -> lambda_create env sigma (t,subst_term sigma e body)) e1_list b in
   let pred_body = beta_applist sigma (abst_B,proj_list) in
-  let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
+  let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
-- 
cgit v1.2.3


From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Dec 2016 10:45:19 +0100
Subject: Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.
---
 tactics/equality.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index d9b6685179..6fcf529c28 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -306,7 +306,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
       else instantiate_lemma_all frzevars gl c t l l2r concl
     in
     let typ = match cls with
-    | None -> pf_nf_concl gl
+    | None -> pf_concl gl
     | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
     in
     let cs = instantiate_lemma typ in
@@ -406,7 +406,7 @@ let type_of_clause cls gl = match cls with
   | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let isatomic = isProd evd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
@@ -1009,7 +1009,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     match find_positions env sigma t1 t2 with
     | Inr _ ->
@@ -1019,7 +1019,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   end }
 
 let onEquality with_evars tac (c,lbindc) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
@@ -1034,7 +1034,7 @@ let onEquality with_evars tac (c,lbindc) =
   end }
 
 let onNegatedEquality with_evars tac =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1302,7 +1302,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let inject_if_homogenous_dependent_pair ty =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
@@ -1458,7 +1458,7 @@ let injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma t1 t2 with
@@ -1567,7 +1567,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1586,7 +1586,7 @@ let cutSubstInConcl l2r eqn =
   end }
 
 let cutSubstInHyp l2r eqn id =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1812,7 +1812,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
           Proofview.tclUNIT ()
     end }
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let ids = find_equations gl in
     tclMAP process ids
   end }
@@ -1822,7 +1822,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 (* Old implementation, not able to manage configurations like a=b, a=t,
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
@@ -1877,7 +1877,7 @@ let rewrite_assumption_cond cond_eq_term cl =
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
     let hyps = Proofview.Goal.hyps gl in
     arec hyps gl
-- 
cgit v1.2.3


From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 tactics/equality.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 53b468bff7..7ae7446c82 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -746,6 +746,7 @@ let find_positions env sigma t1 t2 =
 	    let _,rargs2 = List.chop nparams args2 in
             let (mib,mip) = lookup_mind_specif env ind1 in
             let params1 = List.map EConstr.Unsafe.to_constr params1 in
+            let u1 = EInstance.kind sigma u1 in
             let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in
             let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
             List.flatten
@@ -1324,19 +1325,19 @@ let inject_if_homogenous_dependent_pair ty =
         hd2,ar2 = decompose_app_vect sigma t2 in
     if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
     if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
+    let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
-    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
+    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let inj2 = EConstr.of_constr inj2 in
-    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
+    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
@@ -1783,6 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
+        let u = EInstance.kind sigma u in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
@@ -1834,6 +1836,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let test (_,c) =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let u = EInstance.kind sigma u in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-- 
cgit v1.2.3