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.

---
 plugins/cc/cctac.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b5ca2f50fc..425bb2d6f8 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -58,8 +58,8 @@ let rec decompose_term env sigma t=
 	let tf=decompose_term env sigma f in
 	let targs=Array.map (decompose_term env sigma) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
-    | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
-	let b = Termops.pop _b in
+    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
+	let b = Termops.pop (EConstr.of_constr _b) in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	Appli(Appli(Product (sort_a,sort_b) ,
@@ -86,7 +86,7 @@ let rec decompose_term env sigma t=
 	let p' = Projection.map canon_const p in
 	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
-       let t = Termops.strip_outer_cast t in
+       let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
        if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
@@ -112,8 +112,8 @@ let rec pattern_of_constr env sigma c =
 	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
 	List.fold_left Int.Set.union Int.Set.empty lrels
-    | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
-	let b = Termops.pop _b in
+    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
+	let b = Termops.pop (EConstr.of_constr _b) in
 	let pa,sa = pattern_of_constr env sigma a in
 	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b in
-- 
cgit v1.2.3


From b7fd585b89ac5e0b7770f52739c33fe179f2eed8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Nov 2016 21:36:40 +0100
Subject: Evarsolve API using EConstr.

---
 plugins/cc/cctac.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 425bb2d6f8..36a96fdb5e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -259,7 +259,7 @@ let refresh_universes ty k =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
-    let evm, ty = refresh_type env evm ty in
+    let evm, ty = refresh_type env evm (EConstr.of_constr ty) in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
   end }
 
@@ -376,7 +376,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let identity = Universes.constr_of_global (Lazy.force _I) in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
+    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
@@ -481,7 +481,7 @@ let mk_eq f c1 c2 k =
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
-    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-- 
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.

---
 plugins/cc/cctac.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 36a96fdb5e..58454eedfe 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -50,7 +50,7 @@ let whd_delta env=
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) c
+let sf_of env sigma c = e_sort_of env (ref sigma) (EConstr.of_constr c)
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
@@ -247,7 +247,7 @@ let new_refine c = Proofview.V82.tactic (refine c)
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let evm, _ = Tacmach.New.pf_apply type_of gl c in
+    let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end }
 
@@ -340,7 +340,7 @@ let refute_tac c t1 t2 p =
   end }
 
 let refine_exact_check c gl =
-  let evm, _ = pf_apply type_of gl c in
+  let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
@@ -480,10 +480,10 @@ let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
-    let evm, ty = pf_apply type_of gl c1 in
+    let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
-    let evm, _ =  type_of (pf_env gl) evm term in
+    let evm, _ =  type_of (pf_env gl) evm (EConstr.of_constr term) in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
     end })
-- 
cgit v1.2.3


From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 00:29:02 +0100
Subject: Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
---
 plugins/cc/cctac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 58454eedfe..11da923e18 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -512,7 +512,7 @@ let f_equal =
       | _ -> Proofview.tclUNIT ()
       end
       begin function (e, info) -> match e with
-        | Type_errors.TypeError _ -> Proofview.tclUNIT ()
+        | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT ()
         | e -> Proofview.tclZERO ~info e
       end
   end }
-- 
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.

---
 plugins/cc/ccalgo.ml |  4 ++--
 plugins/cc/cctac.ml  | 11 ++++++-----
 2 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113df..102efe55bc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -508,7 +508,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_unsafe_type_of state.gls trm in
+	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -832,7 +832,7 @@ let complete_one_class state i=
 	    let id = new_state_var etyp state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
-	  (constr_of_term (term state.uf pac.cnode)) in
+	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 11da923e18..7c78f3a17c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -243,7 +243,8 @@ let app_global f args k =
 let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_refine c = Proofview.V82.tactic (refine c)
+let new_refine c = Proofview.V82.tactic (refine (EConstr.of_constr c))
+let refine c = refine (EConstr.of_constr c)
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -265,7 +266,7 @@ let refresh_universes ty k =
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
+  let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check c
@@ -336,7 +337,7 @@ let refute_tac c t1 t2 p =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt1)) k
   end }
 
 let refine_exact_check c gl =
@@ -354,7 +355,7 @@ let convert_to_goal_tac c t1 t2 p =
     let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
 			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt2)) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -376,7 +377,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let identity = Universes.constr_of_global (Lazy.force _I) in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1))) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
-- 
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.

---
 plugins/cc/cctac.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7c78f3a17c..7b023413d6 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -238,17 +238,17 @@ let build_projection intype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
 
 let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
 
-let new_refine c = Proofview.V82.tactic (refine (EConstr.of_constr c))
-let refine c = refine (EConstr.of_constr c)
+let new_refine c = Proofview.V82.tactic (refine c)
+let refine c = refine c
 
 let assert_before n c =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in
+    let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end }
 
@@ -269,7 +269,7 @@ let rec proof_tac p : unit Proofview.tactic =
   let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
   try (* type_of can raise exceptions *)
   match p.p_rule with
-      Ax c -> exact_check c
+      Ax c -> exact_check (EConstr.of_constr c)
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
@@ -333,6 +333,7 @@ let refute_tac c t1 t2 p =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
+  let false_t = EConstr.of_constr false_t in
   let k intype =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
@@ -341,7 +342,7 @@ let refute_tac c t1 t2 p =
   end }
 
 let refine_exact_check c gl =
-  let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in
+  let evm, _ = pf_apply type_of gl c in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
@@ -363,6 +364,8 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
   let tt2=constr_of_term t2 in
   let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
+  let false_t = EConstr.of_constr false_t in
+  let tt2 = EConstr.of_constr tt2 in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
@@ -387,6 +390,7 @@ let discriminate_tac (cstr,u as cstru) p =
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
+            let injt = EConstr.Unsafe.to_constr injt in
             app_global _eq_rect
 		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
@@ -486,7 +490,7 @@ let mk_eq f c1 c2 k =
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm (EConstr.of_constr term) in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-			  (k term)
+			  (k (EConstr.of_constr term))
     end })
 
 let f_equal =
-- 
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.

---
 plugins/cc/cctac.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7b023413d6..a12ef00ec3 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -229,7 +229,8 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype (cstr:pconstructor) special default gls=
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in
+  let body = EConstr.Unsafe.to_constr body in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
-- 
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

---
 plugins/cc/cctac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a12ef00ec3..6295e004e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -87,6 +87,7 @@ let rec decompose_term env sigma t=
 	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
        let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
+       let t = EConstr.Unsafe.to_constr t in
        if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
-- 
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.

---
 plugins/cc/cctac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6295e004e1..130f01e97d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -230,7 +230,7 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype (cstr:pconstructor) special default gls=
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) default in
   let body = EConstr.Unsafe.to_constr body in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
@@ -321,6 +321,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
+         let default = EConstr.of_constr default in
          let proj =
            Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
@@ -388,6 +389,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let injt=app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
@@ -498,6 +500,7 @@ let mk_eq f c1 c2 k =
 let f_equal =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
-- 
cgit v1.2.3


From fa638c3e71752b6a59261776b36f1bed7d9c26d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 12:07:55 +0100
Subject: Cc API using EConstr.

---
 plugins/cc/cctac.ml         | 138 ++++++++++++++++++++++++--------------------
 plugins/cc/cctac.mli        |   2 +-
 plugins/cc/g_congruence.ml4 |   4 +-
 3 files changed, 77 insertions(+), 67 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 130f01e97d..0d48b65d01 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -13,6 +13,7 @@ open Names
 open Inductiveops
 open Declarations
 open Term
+open EConstr
 open Vars
 open Tacmach
 open Tactics
@@ -27,6 +28,10 @@ open Proofview.Notations
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  RelDecl.LocalAssum (na, inj t)
+
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
@@ -39,27 +44,26 @@ let _False = reference ["Init";"Logic"] "False"
 let _True = reference ["Init";"Logic"] "True"
 let _I = reference ["Init";"Logic"] "I"
 
-let whd env=
-  let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let whd env sigma t =
+  Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t
 
-let whd_delta env=
-   let infos=CClosure.create_clos_infos CClosure.all env in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let whd_delta env sigma t =
+  Reductionops.clos_whd_flags CClosure.all env sigma t
 
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) (EConstr.of_constr c)
+let sf_of env sigma c = e_sort_of env (ref sigma) c
 
 let rec decompose_term env sigma t=
-    match kind_of_term (whd env t) with
+    match EConstr.kind sigma (whd env sigma t) with
       App (f,args)->
 	let tf=decompose_term env sigma f in
 	let targs=Array.map (decompose_term env sigma) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
-    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
-	let b = Termops.pop (EConstr.of_constr _b) in
+    | Prod (_,a,_b) when noccurn sigma 1 _b ->
+	let b = Termops.pop _b in
+	let b = EConstr.of_constr b in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	Appli(Appli(Product (sort_a,sort_b) ,
@@ -77,28 +81,27 @@ let rec decompose_term env sigma t=
     | Ind c -> 
 	let (mind,i_ind),u = c in 
 	let canon_mind = mind_of_kn (canonical_mind mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (mkIndU (canon_ind,u)))
+	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
 	let canon_const = constant_of_kn (canonical_con c) in 
-	  (Symb (mkConstU (canon_const,u)))
+	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
 	let canon_const kn = constant_of_kn (canonical_con kn) in 
 	let p' = Projection.map canon_const p in
-	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
+	(Appli (Symb (Constr.mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
-       let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
-       let t = EConstr.Unsafe.to_constr t in
-       if closed0 t then Symb t else raise Not_found
+       let t = Termops.strip_outer_cast sigma t in
+       if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
 
 (* decompose equality in members and type *)
-open Globnames
+open Termops
 
 let atom_of_constr env sigma term =
-  let wh =  (whd_delta env term) in
-  let kot = kind_of_term wh in
+  let wh = whd_delta env sigma term in
+  let kot = EConstr.kind sigma wh in
     match kot with
       App (f,args)->
-	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
+	if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -106,15 +109,16 @@ let atom_of_constr env sigma term =
     | _ -> `Other (decompose_term env sigma term)
 
 let rec pattern_of_constr env sigma c =
-  match kind_of_term (whd env c) with
+  match EConstr.kind sigma (whd env sigma c) with
       App (f,args)->
 	let pf = decompose_term env sigma f in
 	let pargs,lrels = List.split
 	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
 	List.fold_left Int.Set.union Int.Set.empty lrels
-    | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) ->
-	let b = Termops.pop (EConstr.of_constr _b) in
+    | Prod (_,a,_b) when noccurn sigma 1 _b ->
+	let b = Termops.pop _b in
+	let b = EConstr.of_constr b in
 	let pa,sa = pattern_of_constr env sigma a in
 	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b in
@@ -132,19 +136,19 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
+    try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
+	if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
 	  let valid1 =
 	    if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
 	    else if non_trivial patt1 then Normal
-	    else Trivial args.(0)
+	    else Trivial (EConstr.to_constr sigma args.(0))
 	  and valid2 =
 	    if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
 	    else if non_trivial patt2 then Normal
-	    else Trivial args.(0) in
+	    else Trivial (EConstr.to_constr sigma args.(0)) in
 	    if valid1 != Creates_variables
 	      || valid2 != Creates_variables  then
 	      nrels,valid1,patt1,valid2,patt2
@@ -152,28 +156,28 @@ let patterns_of_constr env sigma nrels term=
 	else raise Not_found
 
 let rec quantified_atom_of_constr env sigma nrels term =
-  match kind_of_term (whd_delta env term) with
+  match EConstr.kind sigma (whd_delta env sigma term) with
       Prod (id,atom,ff) -> 
-	if is_global (Lazy.force _False) ff then
+	if is_global sigma (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
+	  quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
 
 let litteral_of_constr env sigma term=
-  match kind_of_term (whd_delta env term) with
+  match EConstr.kind sigma (whd_delta env sigma term) with
     | Prod (id,atom,ff) -> 
-	if is_global (Lazy.force _False) ff then
+	if is_global sigma (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
+	      quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
@@ -197,8 +201,8 @@ let make_prb gls depth additionnal_terms =
       (fun decl ->
          let id = NamedDecl.get_id decl in
 	 begin
-	   let cid=mkVar id in
-	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
+	   let cid=Constr.mkVar id in
+	   match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
 	     | `Other ph ->
@@ -217,7 +221,7 @@ let make_prb gls depth additionnal_terms =
 	     | `Nrule patts -> add_quant state id false patts
 	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with
+      match atom_of_constr env sigma (EConstr.of_constr (pf_concl gls)) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
@@ -230,8 +234,7 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype (cstr:pconstructor) special default gls=
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) default in
-  let body = EConstr.Unsafe.to_constr body in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
@@ -240,10 +243,10 @@ let build_projection intype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
 
 let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 let refine c = refine c
@@ -259,20 +262,24 @@ let refresh_type env evm ty =
 			      (Some false) env evm ty
 
 let refresh_universes ty k =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
-    let evm, ty = refresh_type env evm (EConstr.of_constr ty) in
-    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
+    let evm, ty = refresh_type env evm ty in
+    let ty = EConstr.of_constr ty in
+    Sigma.Unsafe.of_pair (k ty, evm)
   end }
 
+let constr_of_term c = EConstr.of_constr (constr_of_term c)
+
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
+  let type_of t = EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t) in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
     | SymAx c ->
+        let c = EConstr.of_constr c in
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
 	refresh_universes (type_of l) (fun typ ->
@@ -321,7 +328,6 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
-         let default = EConstr.of_constr default in
          let proj =
            Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
@@ -336,12 +342,11 @@ let refute_tac c t1 t2 p =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
-  let false_t = EConstr.of_constr false_t in
   let k intype =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt1)) k
+  in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt1)) k
   end }
 
 let refine_exact_check c gl =
@@ -359,7 +364,7 @@ let convert_to_goal_tac c t1 t2 p =
     let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
 			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt2)) k
+  in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt2)) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -367,8 +372,6 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
   let tt2=constr_of_term t2 in
   let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
-  let false_t = EConstr.of_constr false_t in
-  let tt2 = EConstr.of_constr tt2 in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
@@ -381,20 +384,21 @@ let discriminate_tac (cstr,u as cstru) p =
     let concl = Proofview.Goal.concl gl in
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
     let identity = Universes.constr_of_global (Lazy.force _I) in
+    let identity = EConstr.of_constr identity in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
+    let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1))) in
+    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+    let intype = EConstr.of_constr intype in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
-    let concl = EConstr.Unsafe.to_constr concl in
     let injt=app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
-            let injt = EConstr.Unsafe.to_constr injt in
             app_global _eq_rect
 		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
@@ -410,7 +414,7 @@ let build_term_to_complete uf meta pac =
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
   let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applistc (mkConstructU cinfo.ci_constr) all_args
+    applist (mkConstructU cinfo.ci_constr, all_args)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -448,7 +452,7 @@ let cc_tactic depth additionnal_terms =
 		   str "\"congruence with (" ++
 		     prlist_with_sep
 		     (fun () -> str ")" ++ spc () ++ str "(")
-		     (Termops.print_constr_env env)
+		     (EConstr.Unsafe.to_constr %> Termops.print_constr_env env)
 		     terms_to_complete ++
 		     str ")\","
 		 end ++
@@ -459,10 +463,13 @@ let cc_tactic depth additionnal_terms =
 	    let ta=term uf dis.lhs and tb=term uf dis.rhs in
 	    match dis.rule with
 	      Goal -> proof_tac p
-	    | Hyp id -> refute_tac id ta tb p
+	    | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
 	    | HeqG id ->
+                let id = EConstr.of_constr id in
 		convert_to_goal_tac id ta tb p
 	    | HeqnH (ida,idb) ->
+                let ida = EConstr.of_constr ida in
+                let idb = EConstr.of_constr idb in
 		convert_to_hyp_tac ida ta idb tb p
   end }
 
@@ -487,20 +494,23 @@ let congruence_tac depth l =
 
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+  let fc = EConstr.of_constr fc in
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
-    let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in
-    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
+    let evm, ty = pf_apply type_of gl c1 in
+    let ty = EConstr.of_constr ty in
+    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+    let ty = EConstr.of_constr ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
-    let evm, _ =  type_of (pf_env gl) evm (EConstr.of_constr term) in
+    let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-			  (k (EConstr.of_constr term))
+			  (k term)
     end })
 
 let f_equal =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let concl = EConstr.Unsafe.to_constr concl in
+    let sigma = Tacmach.New.project gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
@@ -509,9 +519,9 @@ let f_equal =
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
-      begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
-	  begin match kind_of_term t, kind_of_term t' with
+      begin match EConstr.kind sigma concl with
+      | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
+	  begin match EConstr.kind sigma t, EConstr.kind sigma t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
 		if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 7c1d9f1c07..de6eb982ee 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open EConstr
 open Proof_type
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 6f6811334d..b787e824f8 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -18,9 +18,9 @@ DECLARE PLUGIN "cc_plugin"
 TACTIC EXTEND cc
  [ "congruence" ] -> [ congruence_tac 1000 [] ]
  |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
+ |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 (List.map EConstr.of_constr l) ]
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
-   [ congruence_tac n l ]
+   [ congruence_tac n (List.map EConstr.of_constr l) ]
 END
 
 TACTIC EXTEND f_equal
-- 
cgit v1.2.3


From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 15:50:17 +0100
Subject: Removing some return type compatibility layers in Termops.

---
 plugins/cc/cctac.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0d48b65d01..7a99c45a8b 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -63,7 +63,6 @@ let rec decompose_term env sigma t=
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
     | Prod (_,a,_b) when noccurn sigma 1 _b ->
 	let b = Termops.pop _b in
-	let b = EConstr.of_constr b in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	Appli(Appli(Product (sort_a,sort_b) ,
@@ -118,7 +117,6 @@ let rec pattern_of_constr env sigma c =
 	List.fold_left Int.Set.union Int.Set.empty lrels
     | Prod (_,a,_b) when noccurn sigma 1 _b ->
 	let b = Termops.pop _b in
-	let b = EConstr.of_constr b in
 	let pa,sa = pattern_of_constr env sigma a in
 	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b 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

---
 plugins/cc/cctac.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7a99c45a8b..a4ed4798ae 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -264,7 +264,6 @@ let refresh_universes ty k =
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
     let evm, ty = refresh_type env evm ty in
-    let ty = EConstr.of_constr ty in
     Sigma.Unsafe.of_pair (k ty, evm)
   end }
 
@@ -387,7 +386,6 @@ let discriminate_tac (cstr,u as cstru) p =
     let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
     let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
-    let intype = EConstr.of_constr intype in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
@@ -496,9 +494,7 @@ let mk_eq f c1 c2 k =
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
-    let ty = EConstr.of_constr ty in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
-    let ty = EConstr.of_constr ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-- 
cgit v1.2.3


From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 18:18:17 +0100
Subject: Ltac now uses evar-based constrs.

---
 plugins/cc/ccalgo.ml        | 8 ++++----
 plugins/cc/cctac.ml         | 3 ++-
 plugins/cc/g_congruence.ml4 | 4 ++--
 3 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 102efe55bc..0a980c03b7 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -497,10 +497,10 @@ let rec inst_pattern subst = function
 	   args t
 
 let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
 let pr_term t = str "[" ++
-  Termops.print_constr (constr_of_term t) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -615,7 +615,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
@@ -623,7 +623,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a4ed4798ae..62892973d4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -414,6 +414,7 @@ let build_term_to_complete uf meta pac =
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
     let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
@@ -448,7 +449,7 @@ let cc_tactic depth additionnal_terms =
 		   str "\"congruence with (" ++
 		     prlist_with_sep
 		     (fun () -> str ")" ++ spc () ++ str "(")
-		     (EConstr.Unsafe.to_constr %> Termops.print_constr_env env)
+		     (Termops.print_constr_env env sigma)
 		     terms_to_complete ++
 		     str ")\","
 		 end ++
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index b787e824f8..6f6811334d 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -18,9 +18,9 @@ DECLARE PLUGIN "cc_plugin"
 TACTIC EXTEND cc
  [ "congruence" ] -> [ congruence_tac 1000 [] ]
  |[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 (List.map EConstr.of_constr l) ]
+ |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
-   [ congruence_tac n (List.map EConstr.of_constr l) ]
+   [ congruence_tac n l ]
 END
 
 TACTIC EXTEND f_equal
-- 
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.

---
 plugins/cc/ccalgo.ml |  8 +++++---
 plugins/cc/cctac.ml  | 10 +++++-----
 2 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 0a980c03b7..aedcb75750 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -452,8 +452,9 @@ and applist_projection c l =
       applistc (mkProj (p, hd)) tl)
   | _ -> applistc c l
 
-let rec canonize_name c =
-  let func =  canonize_name in
+let rec canonize_name sigma c =
+  let c = EConstr.Unsafe.to_constr c in
+  let func c = canonize_name sigma (EConstr.of_constr c) in
     match kind_of_term c with
       | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
@@ -509,7 +510,7 @@ let rec add_term state t=
 	  let b=next uf in
           let trm = constr_of_term t in
 	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
-	  let typ = canonize_name typ in
+	  let typ = canonize_name (project state.gls) typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
@@ -833,6 +834,7 @@ let complete_one_class state i=
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
 	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+        let _c = EConstr.Unsafe.to_constr _c in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 62892973d4..2ab4dced4d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -219,7 +219,7 @@ let make_prb gls depth additionnal_terms =
 	     | `Nrule patts -> add_quant state id false patts
 	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (EConstr.of_constr (pf_concl gls)) with
+      match atom_of_constr env sigma (pf_concl gls) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
@@ -271,7 +271,7 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let type_of t = EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t) in
+  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
@@ -343,7 +343,7 @@ let refute_tac c t1 t2 p =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt1)) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
 let refine_exact_check c gl =
@@ -361,7 +361,7 @@ let convert_to_goal_tac c t1 t2 p =
     let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
 			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
-  in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt2)) k
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
-- 
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

---
 plugins/cc/cctac.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2ab4dced4d..53c4501169 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -241,10 +241,10 @@ let build_projection intype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (EConstr.of_constr fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 let refine c = refine c
@@ -491,7 +491,6 @@ let congruence_tac depth l =
 
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
-  let fc = EConstr.of_constr fc in
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
-- 
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.
---
 plugins/cc/cctac.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 53c4501169..5d894c6774 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -28,10 +28,6 @@ open Proofview.Notations
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  RelDecl.LocalAssum (na, inj t)
-
 let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
@@ -160,7 +156,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma (succ nrels) ff
+	  quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
@@ -175,7 +171,7 @@ let litteral_of_constr env sigma term=
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (Environ.push_rel (local_assum (id,atom)) env) sigma 1 ff
+	      quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
-- 
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.
---
 plugins/cc/cctac.ml | 44 +++++++++++++++++++++++---------------------
 1 file changed, 23 insertions(+), 21 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5d894c6774..c9c904e350 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -182,9 +182,10 @@ let litteral_of_constr env sigma term=
 (* store all equalities from the context *)
 
 let make_prb gls depth additionnal_terms =
+  let open Tacmach.New in
   let env=pf_env gls in
-  let sigma=sig_sig gls in
-  let state = empty depth gls in
+  let sigma=project gls in
+  let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in
   let pos_hyps = ref [] in
   let neg_hyps =ref [] in
     List.iter
@@ -196,7 +197,7 @@ let make_prb gls depth additionnal_terms =
          let id = NamedDecl.get_id decl in
 	 begin
 	   let cid=Constr.mkVar id in
-	   match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with
+	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
 	     | `Other ph ->
@@ -213,7 +214,7 @@ let make_prb gls depth additionnal_terms =
 		 neg_hyps:=(cid,nh):: !neg_hyps
 	     | `Rule patts -> add_quant state id true patts
 	     | `Nrule patts -> add_quant state id false patts
-	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
+	 end) (Proofview.Goal.hyps gls);
     begin
       match atom_of_constr env sigma (pf_concl gls) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
@@ -227,6 +228,7 @@ let make_prb gls depth additionnal_terms =
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
 let build_projection intype (cstr:pconstructor) special default gls=
+  let open Tacmach.New in
   let ci= (snd(fst cstr)) in
   let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
@@ -266,7 +268,7 @@ let refresh_universes ty k =
 let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
@@ -296,7 +298,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	refresh_universes (type_of tf1) (fun typf ->
 	refresh_universes (type_of tx1) (fun typx ->
 	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
-        let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
+        let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
 	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
@@ -322,7 +324,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
          let proj =
-           Tacmach.New.of_old (build_projection intype cstr special default) gl
+           build_projection intype cstr special default gl
          in
 	 let injt=
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
@@ -331,9 +333,9 @@ let rec proof_tac p : unit Proofview.tactic =
   end }
 
 let refute_tac c t1 t2 p =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+  let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
   let k intype =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
@@ -347,12 +349,12 @@ let refine_exact_check c gl =
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let k sort =
     let neweq= new_app_global _eq [|sort;tt1;tt2|] in
-    let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
-    let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
+    let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
     let identity=mkLambda (Name x,sort,mkRel 1) in
     let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
@@ -361,9 +363,9 @@ let convert_to_goal_tac c t1 t2 p =
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let tt2=constr_of_term t2 in
-  let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
+  let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
@@ -371,11 +373,11 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
   end }
 
 let discriminate_tac (cstr,u as cstru) p =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
     let identity = Universes.constr_of_global (Lazy.force _I) in
     let identity = EConstr.of_constr identity in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
@@ -385,8 +387,8 @@ let discriminate_tac (cstr,u as cstru) p =
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
-    let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
-    let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
+    let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
+    let proj = build_projection intype cstru trivial concl gl in
     let injt=app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
@@ -409,11 +411,11 @@ let build_term_to_complete uf meta pac =
     applist (mkConstructU cinfo.ci_constr, all_args)
 
 let cc_tactic depth additionnal_terms =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
-    let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
+    let state = make_prb gl depth additionnal_terms in
     let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
     let _ = debug (fun () -> Pp.str "Computation completed.") in
@@ -498,7 +500,7 @@ let mk_eq f c1 c2 k =
     end })
 
 let f_equal =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let cut_eq c1 c2 =
-- 
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.
---
 plugins/cc/cctac.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c9c904e350..2d9dec095a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -66,6 +66,7 @@ let rec decompose_term env sigma t=
 	      decompose_term env sigma b)
     | Construct c ->
 	let (((mind,i_ind),i_con),u)= c in 
+	let u = EInstance.kind sigma u in
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
@@ -75,9 +76,11 @@ let rec decompose_term env sigma t=
 		       ci_nhyps=nargs-oib.mind_nparams}
     | Ind c -> 
 	let (mind,i_ind),u = c in 
+	let u = EInstance.kind sigma u in
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
+	let u = EInstance.kind sigma u in
 	let canon_const = constant_of_kn (canonical_con c) in 
 	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
@@ -408,7 +411,8 @@ let build_term_to_complete uf meta pac =
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
   let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applist (mkConstructU cinfo.ci_constr, all_args)
+  let (kn, u) = cinfo.ci_constr in
+    applist (mkConstructU (kn, EInstance.make u), all_args)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter { enter = begin fun gl ->
-- 
cgit v1.2.3