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.

---
 pretyping/inductiveops.ml | 53 +++++++++++++++++++++++++++--------------------
 1 file changed, 31 insertions(+), 22 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 29f57144a9..a3cca2ad87 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -444,15 +444,17 @@ let build_branch_type env dep p cs =
 
 (**************************************************)
 
-let extract_mrectype t =
-  let (t, l) = decompose_app t in
-  match kind_of_term t with
-    | Ind ind -> (ind, l)
+let extract_mrectype sigma t =
+  let open EConstr in
+  let (t, l) = decompose_app sigma t in
+  match EConstr.kind sigma t with
+    | Ind ind -> (ind, List.map EConstr.Unsafe.to_constr l)
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let (t, l) = decompose_appvect (whd_all env sigma c) in
-  match kind_of_term t with
+  let open EConstr in
+  let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in
+  match EConstr.kind sigma (EConstr.of_constr t) with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
@@ -460,28 +462,34 @@ let find_mrectype env sigma c =
   let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v)
 
 let find_rectype env sigma c =
-  let (t, l) = decompose_app (whd_all env sigma c) in
-  match kind_of_term t with
+  let open EConstr in
+  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  match EConstr.kind sigma t with
     | Ind (ind,u as indu) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
         if mib.mind_nparams > List.length l then raise Not_found;
+        let l = List.map EConstr.Unsafe.to_constr l in
         let (par,rargs) = List.chop mib.mind_nparams l in
         IndType((indu, par),rargs)
     | _ -> raise Not_found
 
 let find_inductive env sigma c =
-  let (t, l) = decompose_app (whd_all env sigma c) in
-  match kind_of_term t with
+  let open EConstr in
+  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
+        let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env sigma c =
-  let (t, l) = decompose_app (whd_all env sigma c) in
-  match kind_of_term t with
+  let open EConstr in
+  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
+        let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
 
@@ -490,12 +498,12 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the Case
    and Inversion (case_then_using et case_nodep_then_using) tactics. *)
 
-let is_predicate_explicitly_dep env pred arsign =
+let is_predicate_explicitly_dep env sigma pred arsign =
   let rec srec env pval arsign =
-    let pv' = whd_all env Evd.empty pval in
-    match kind_of_term pv', arsign with
+    let pv' = EConstr.of_constr (whd_all env sigma pval) in
+    match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
-	  srec (push_rel_assum (na,t) env) b arsign
+	  srec (push_rel_assum (na, EConstr.Unsafe.to_constr t) env) b arsign
       | Lambda (na,_,t), _ ->
 
        (* The following code has an impact on the introduction names
@@ -525,11 +533,11 @@ let is_predicate_explicitly_dep env pred arsign =
 
       | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
   in
-  srec env pred arsign
+  srec env (EConstr.of_constr pred) arsign
 
-let is_elim_predicate_explicitly_dependent env pred indf =
+let is_elim_predicate_explicitly_dependent env sigma pred indf =
   let arsign,_ = get_arity env indf in
-  is_predicate_explicitly_dep env pred arsign
+  is_predicate_explicitly_dep env sigma pred arsign
 
 let set_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
@@ -545,7 +553,7 @@ let set_pattern_names env ind brv =
       mip.mind_nf_lc in
   Array.map2 (set_names env) arities brv
 
-let type_case_branches_with_names env indspec p c =
+let type_case_branches_with_names env sigma indspec p c =
   let (ind,args) = indspec in
   let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
   let nparams = mib.mind_nparams in
@@ -554,7 +562,7 @@ let type_case_branches_with_names env indspec p c =
   (* Build case type *)
   let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
-  if is_elim_predicate_explicitly_dependent env p (ind,params) then
+  if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
   else (lbrty, conclty)
 
@@ -600,7 +608,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
   | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity
   | TemplateArity ar ->
-    let _,scl = Reduction.dest_arity env conclty in
+    let _,scl = splay_arity env sigma conclty in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
@@ -609,6 +617,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
       !evdref, mkArity (List.rev ctx,scl)
 
 let type_of_projection_knowing_arg env sigma p c ty =
+  let c = EConstr.Unsafe.to_constr c in
   let IndType(pars,realargs) =
     try find_rectype env sigma ty
     with Not_found ->
-- 
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.

---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a3cca2ad87..a9184777d0 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -606,7 +606,7 @@ let rec instantiate_universes env evdref scl is = function
 
 let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
-  | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity
+  | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
     let _,scl = splay_arity env sigma conclty in
     let ctx = List.rev mip.mind_arity_ctxt in
@@ -614,7 +614,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
     let ctx =
       instantiate_universes
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
-      !evdref, mkArity (List.rev ctx,scl)
+      !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
 let type_of_projection_knowing_arg env sigma p c ty =
   let c = EConstr.Unsafe.to_constr c in
-- 
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.

---
 pretyping/inductiveops.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a9184777d0..a93f2846b5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -343,24 +343,25 @@ let get_projections env (ind,params) =
     | Some (Some (id, projs, pbs)) -> Some projs
     | _ -> None
 
-let make_case_or_project env indf ci pred c branches =
+let make_case_or_project env sigma indf ci pred c branches =
+  let open EConstr in
   let projs = get_projections env indf in
   match projs with
   | None -> (mkCase (ci, pred, c, branches))
   | Some ps ->
      assert(Array.length branches == 1);
      let () =
-       let _, _, t = destLambda pred in
+       let _, _, t = destLambda sigma pred in
        let (ind, _), _ = dest_ind_family indf in
        let mib, _ = Inductive.lookup_mind_specif env ind in
-       if (* dependent *) not (noccurn 1 t) &&
+       if (* dependent *) not (Vars.noccurn sigma 1 t) &&
           not (has_dependent_elim mib) then
        user_err ~hdr:"make_case_or_project"
 		    Pp.(str"Dependent case analysis not allowed" ++
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
      let branch = branches.(0) in
-     let ctx, br = decompose_lam_n_assum (Array.length ps) branch in
+     let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
      let n, subst =
        List.fold_right
          (fun decl (i, subst) ->
@@ -368,9 +369,9 @@ let make_case_or_project env indf ci pred c branches =
 	  | LocalAssum (na, t) ->
 	     let t = mkProj (Projection.make ps.(i) true, c) in
 	     (i + 1, t :: subst)
-	  | LocalDef (na, b, t) -> (i, substl subst b :: subst))
+	  | LocalDef (na, b, t) -> (i, Vars.substl subst (EConstr.of_constr b) :: subst))
 	 ctx (0, [])
-     in substl subst br
+     in Vars.substl subst br
 
 (* substitution in a signature *)
 
-- 
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.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a93f2846b5..e30ba21fd1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -504,7 +504,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
     let pv' = EConstr.of_constr (whd_all env sigma pval) in
     match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
-	  srec (push_rel_assum (na, EConstr.Unsafe.to_constr t) env) b arsign
+	  srec (push_rel_assum (na, t) env) b arsign
       | Lambda (na,_,t), _ ->
 
        (* The following code has an impact on the introduction names
-- 
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.

---
 pretyping/inductiveops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e30ba21fd1..98b267cfd4 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -556,6 +556,7 @@ let set_pattern_names env ind brv =
 
 let type_case_branches_with_names env sigma indspec p c =
   let (ind,args) = indspec in
+  let args = List.map EConstr.Unsafe.to_constr args in
   let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
   let nparams = mib.mind_nparams in
   let (params,realargs) = List.chop nparams args in
-- 
cgit v1.2.3


From 7b43de20a4acd7c9da290f038d9a16fe67eccd59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:59:07 +0100
Subject: Leminv API using EConstr.

---
 pretyping/inductiveops.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 98b267cfd4..cb8b253232 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -58,21 +58,23 @@ let lift_inductive_family n = liftn_inductive_family n 1
 let substnl_ind_family l n = map_ind_family (substnl l n)
 
 
-type inductive_type = IndType of inductive_family * constr list
+type inductive_type = IndType of inductive_family * EConstr.constr list
 
 let make_ind_type (indf, realargs) = IndType (indf,realargs)
 let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
 
 let map_inductive_type f (IndType (indf, realargs)) =
-  IndType (map_ind_family f indf, List.map f realargs)
+  let f' c = EConstr.Unsafe.to_constr (f (EConstr.of_constr c)) in
+  IndType (map_ind_family f' indf, List.map f realargs)
 
-let liftn_inductive_type n d = map_inductive_type (liftn n d)
+let liftn_inductive_type n d = map_inductive_type (EConstr.Vars.liftn n d)
 let lift_inductive_type n = liftn_inductive_type n 1
 
-let substnl_ind_type l n = map_inductive_type (substnl l n)
+let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n)
 
 let mkAppliedInd (IndType ((ind,params), realargs)) =
-  applist (mkIndU ind,params@realargs)
+  let open EConstr in
+  applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs)
 
 (* Does not consider imbricated or mutually recursive types *)
 let mis_is_recursive_subset listind rarg =
@@ -471,7 +473,7 @@ let find_rectype env sigma c =
         if mib.mind_nparams > List.length l then raise Not_found;
         let l = List.map EConstr.Unsafe.to_constr l in
         let (par,rargs) = List.chop mib.mind_nparams l in
-        IndType((indu, par),rargs)
+        IndType((indu, par),List.map EConstr.of_constr rargs)
     | _ -> raise Not_found
 
 let find_inductive env sigma c =
-- 
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

---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cb8b253232..9c5a2e894a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -451,13 +451,13 @@ let extract_mrectype sigma t =
   let open EConstr in
   let (t, l) = decompose_app sigma t in
   match EConstr.kind sigma t with
-    | Ind ind -> (ind, List.map EConstr.Unsafe.to_constr l)
+    | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
   let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in
-  match EConstr.kind sigma (EConstr.of_constr t) with
+  match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
-- 
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.

---
 pretyping/inductiveops.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 9c5a2e894a..120adb9fef 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -456,7 +456,7 @@ let extract_mrectype sigma t =
 
 let find_mrectype_vect env sigma c =
   let open EConstr in
-  let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
@@ -466,7 +466,7 @@ let find_mrectype env sigma c =
 
 let find_rectype env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind (ind,u as indu) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -478,7 +478,7 @@ let find_rectype env sigma c =
 
 let find_inductive env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
@@ -488,7 +488,7 @@ let find_inductive env sigma c =
 
 let find_coinductive env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
@@ -503,7 +503,7 @@ let find_coinductive env sigma c =
 
 let is_predicate_explicitly_dep env sigma pred arsign =
   let rec srec env pval arsign =
-    let pv' = EConstr.of_constr (whd_all env sigma pval) in
+    let pv' = whd_all env sigma pval in
     match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
 	  srec (push_rel_assum (na, t) env) b arsign
-- 
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.

---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 120adb9fef..1dcd6399e7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -443,7 +443,7 @@ let build_branch_type env dep p cs =
       (applist (base,[build_dependent_constructor cs]))
       cs.cs_args
   else
-    it_mkProd_or_LetIn base cs.cs_args
+    Term.it_mkProd_or_LetIn base cs.cs_args
 
 (**************************************************)
 
@@ -575,7 +575,7 @@ let arity_of_case_predicate env (ind,params) dep k =
   let arsign,_ = get_arity env (ind,params) in
   let mind = build_dependent_inductive env (ind,params) in
   let concl = if dep then mkArrow mind (mkSort k) else mkSort k in
-  it_mkProd_or_LetIn concl arsign
+  Term.it_mkProd_or_LetIn concl arsign
 
 (***********************************************)
 (* Inferring the sort of parameters of a polymorphic inductive type
-- 
cgit v1.2.3


From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 15:30:02 +0100
Subject: Introducing contexts parameterized by the inner term type.

This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1dcd6399e7..c00ceb02e2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -411,14 +411,14 @@ let build_dependent_constructor cs =
   applist
     (mkConstructU cs.cs_cstr,
      (List.map (lift cs.cs_nargs) cs.cs_params)
-      @(Context.Rel.to_extended_list 0 cs.cs_args))
+      @(Context.Rel.to_extended_list mkRel 0 cs.cs_args))
 
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
   let nrealargs = List.length arsign in
   applist
     (mkIndU ind,
-     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign))
+     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list mkRel 0 arsign))
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-- 
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.
---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c00ceb02e2..3191a58ff0 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -371,7 +371,7 @@ let make_case_or_project env sigma indf ci pred c branches =
 	  | LocalAssum (na, t) ->
 	     let t = mkProj (Projection.make ps.(i) true, c) in
 	     (i + 1, t :: subst)
-	  | LocalDef (na, b, t) -> (i, Vars.substl subst (EConstr.of_constr b) :: subst))
+	  | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
 	 ctx (0, [])
      in Vars.substl subst br
 
-- 
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.
---
 pretyping/inductiveops.ml | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3191a58ff0..9e823ab4c5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -422,26 +422,29 @@ let build_dependent_inductive env ((ind, params) as indf) =
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-let make_arity_signature env dep indf =
+let make_arity_signature env sigma dep indf =
   let (arsign,_) = get_arity env indf in
+  let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
   if dep then
     (* We need names everywhere *)
-    Namegen.name_context env
-      ((LocalAssum (Anonymous,build_dependent_inductive env indf))::arsign)
+    Namegen.name_context env sigma
+      ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign)
       (* Costly: would be better to name once for all at definition time *)
   else
     (* No need to enforce names *)
     arsign
 
-let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
+let make_arity env sigma dep indf s =
+  let open EConstr in
+  it_mkProd_or_LetIn (mkSort s) (make_arity_signature env sigma dep indf)
 
 (* [p] is the predicate and [cs] a constructor summary *)
-let build_branch_type env dep p cs =
+let build_branch_type env sigma dep p cs =
   let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
   if dep then
-    Namegen.it_mkProd_or_LetIn_name env
-      (applist (base,[build_dependent_constructor cs]))
-      cs.cs_args
+    EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma
+      (EConstr.of_constr (applist (base,[build_dependent_constructor cs])))
+      (List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) cs.cs_args))
   else
     Term.it_mkProd_or_LetIn base cs.cs_args
 
@@ -542,11 +545,12 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf =
   let arsign,_ = get_arity env indf in
   is_predicate_explicitly_dep env sigma pred arsign
 
-let set_names env n brty =
-  let (ctxt,cl) = decompose_prod_n_assum n brty in
-  Namegen.it_mkProd_or_LetIn_name env cl ctxt
+let set_names env sigma n brty =
+  let open EConstr in
+  let (ctxt,cl) = decompose_prod_n_assum sigma n brty in
+  EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt)
 
-let set_pattern_names env ind brv =
+let set_pattern_names env sigma ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
@@ -554,7 +558,7 @@ let set_pattern_names env ind brv =
         Context.Rel.length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
-  Array.map2 (set_names env) arities brv
+  Array.map2 (set_names env sigma) arities brv
 
 let type_case_branches_with_names env sigma indspec p c =
   let (ind,args) = indspec in
@@ -567,7 +571,7 @@ let type_case_branches_with_names env sigma indspec p c =
   let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
-    (set_pattern_names env (fst ind) lbrty, conclty)
+    (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty)
   else (lbrty, conclty)
 
 (* Type of Case predicates *)
-- 
cgit v1.2.3


From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:20:25 +0200
Subject: Actually exporting delayed universes in the EConstr implementation.

For now we only normalize sorts, and we leave instances for the next
commit.
---
 pretyping/inductiveops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d5967c4bfc..88c492f03d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -617,6 +617,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
     let _,scl = splay_arity env sigma conclty in
+    let scl = EConstr.ESorts.kind sigma scl in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
-- 
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.
---
 pretyping/inductiveops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 88c492f03d..5b42add285 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -74,6 +74,7 @@ let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n)
 
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   let open EConstr in
+  let ind = on_snd EInstance.make ind in
   applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs)
 
 (* Does not consider imbricated or mutually recursive types *)
@@ -471,11 +472,12 @@ let find_rectype env sigma c =
   let open EConstr in
   let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
-    | Ind (ind,u as indu) ->
+    | Ind (ind,u) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
         if mib.mind_nparams > List.length l then raise Not_found;
         let l = List.map EConstr.Unsafe.to_constr l in
         let (par,rargs) = List.chop mib.mind_nparams l in
+        let indu = (ind, EInstance.kind sigma u) in
         IndType((indu, par),List.map EConstr.of_constr rargs)
     | _ -> raise Not_found
 
-- 
cgit v1.2.3