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/typing.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e79e3d46f1..e3d1c17413 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl =
   Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
 
 let e_type_judgment env evdref j =
-  match kind_of_term (whd_all env !evdref j.uj_type) with
+  match kind_of_term (whd_all env !evdref (EConstr.of_constr j.uj_type)) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -54,7 +54,7 @@ let e_judge_of_apply env evdref funj argjv =
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
         uj_type = typ }
   | hj::restjl ->
-      match kind_of_term (whd_all env !evdref typ) with
+      match kind_of_term (whd_all env !evdref (EConstr.of_constr typ)) with
       | Prod (_,c1,c2) ->
 	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -87,7 +87,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let allowed_sorts = elim_sorts specif in
   let error () = error_elim_arity env ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = whd_all env !evdref pt in
+    let pt' = whd_all env !evdref (EConstr.of_constr pt) in
     match kind_of_term pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 a1') then error ();
@@ -113,12 +113,12 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let () = e_is_correct_arity env evdref c pj ind specif params in
   let lc = build_branches_type ind specif params p in
   let n = (snd specif).Declarations.mind_nrealdecls in
-  let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in
+  let ty = whd_betaiota !evdref (EConstr.of_constr (lambda_applist_assum (n+1) p (realargs@[c]))) in
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
   let indspec =
-    try find_mrectype env !evdref cj.uj_type
+    try find_mrectype env !evdref (EConstr.of_constr cj.uj_type)
     with Not_found -> error_case_not_inductive env cj in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
@@ -139,7 +139,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
+  let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
-- 
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/typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e3d1c17413..acfe05f24d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -138,7 +138,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let pj = Retyping.get_judgment_of env sigma p in
+  let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in
   let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
-- 
cgit v1.2.3


From 147afe827dc83602cc160a8b1357e84ecea910ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Nov 2016 20:13:32 +0100
Subject: Evardefine API using EConstr.

---
 pretyping/typing.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index acfe05f24d..db31541cd0 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl =
   Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
 
 let e_type_judgment env evdref j =
-  match kind_of_term (whd_all env !evdref (EConstr.of_constr j.uj_type)) with
+  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -49,26 +49,27 @@ let e_assumption_of_judgment env evdref j =
     error_assumption env j
 
 let e_judge_of_apply env evdref funj argjv =
+  let open EConstr in
   let rec apply_rec n typ = function
   | [] ->
-      { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
-        uj_type = typ }
+      { uj_val  = Constr.mkApp (j_val funj, Array.map j_val argjv);
+        uj_type = EConstr.Unsafe.to_constr typ }
   | hj::restjl ->
-      match kind_of_term (whd_all env !evdref (EConstr.of_constr typ)) with
+      match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
-	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
-	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+	 if Evarconv.e_cumul env evdref hj.uj_type (EConstr.Unsafe.to_constr c1) then
+	   apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
 	 else
-	   error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv
+	   error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
       | Evar ev ->
 	  let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
           evdref := evd';
-          let (_,_,c2) = destProd t in
-	  apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+          let (_,_,c2) = destProd evd' t in
+	  apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
       | _ ->
 	  error_cant_apply_not_functional env funj argjv
   in
-  apply_rec 1 funj.uj_type (Array.to_list argjv)
+  apply_rec 1 (EConstr.of_constr funj.uj_type) (Array.to_list argjv)
 
 let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
-- 
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.

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

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index db31541cd0..1dcb5f9451 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -309,7 +309,7 @@ let type_of ?(refresh=false) env evd c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type)
     else !evdref, j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
@@ -317,7 +317,7 @@ let e_type_of ?(refresh=false) env evdref c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
+      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) in
       let () = evdref := evd in
       c
     else j.uj_type
-- 
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.

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

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1dcb5f9451..64264cf087 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -57,7 +57,7 @@ let e_judge_of_apply env evdref funj argjv =
   | hj::restjl ->
       match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
-	 if Evarconv.e_cumul env evdref hj.uj_type (EConstr.Unsafe.to_constr c1) then
+	 if Evarconv.e_cumul env evdref (EConstr.of_constr hj.uj_type) c1 then
 	   apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
 	 else
 	   error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
@@ -75,7 +75,7 @@ let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
     error_number_branches env cj (Array.length explft);
   for i = 0 to Array.length explft - 1 do
-    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
+    if not (Evarconv.e_cumul env evdref (EConstr.of_constr lfj.(i).uj_type) (EConstr.of_constr explft.(i))) then
       error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
   done
 
@@ -91,7 +91,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
     let pt' = whd_all env !evdref (EConstr.of_constr pt) in
     match kind_of_term pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref a1 a1') then error ();
+        if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error ();
         srec (push_rel (LocalAssum (na1,a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
@@ -131,8 +131,8 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
-        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
+        if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
+		  (EConstr.of_constr (lift lt lar.(i)))) then
           Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
             i lna vdefj lar
       done
@@ -150,7 +150,7 @@ let check_allowed_sort env sigma ind c p =
 
 let e_judge_of_cast env evdref cj k tj =
   let expected_type = tj.utj_val in
-  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr cj.uj_type) (EConstr.of_constr expected_type)) then
     error_actual_type env cj expected_type;
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
@@ -282,7 +282,7 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then
     error_actual_type env j (nf_evar !evdref t)
 
 (* Type of a constr *)
@@ -328,4 +328,4 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars e_solve_evars
+let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c)))
-- 
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.

---
 pretyping/typing.ml | 80 ++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 51 insertions(+), 29 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 64264cf087..c948f9b9a7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -20,6 +20,11 @@ open Typeops
 open Arguments_renaming
 open Context.Rel.Declaration
 
+let push_rec_types pfix env =
+  let (i, c, t) = pfix in
+  let inj c = EConstr.Unsafe.to_constr c in
+  push_rec_types (i, Array.map inj c, Array.map inj t) env
+
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
@@ -28,12 +33,12 @@ let meta_type evd mv =
 
 let constant_type_knowing_parameters env cst jl =
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  type_of_constant_knowing_parameters_in env cst paramstyp
+  EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
 
 let inductive_type_knowing_parameters env (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+  EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
   match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
@@ -44,7 +49,7 @@ let e_type_judgment env evdref j =
     | _ -> error_not_type env j
 
 let e_assumption_of_judgment env evdref j =
-  try (e_type_judgment env evdref j).utj_val
+  try EConstr.of_constr (e_type_judgment env evdref j).utj_val
   with TypeError _ ->
     error_assumption env j
 
@@ -84,27 +89,28 @@ let max_sort l =
   if Sorts.List.mem InSet l then InSet else InProp
 
 let e_is_correct_arity env evdref c pj ind specif params =
+  let open EConstr in
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
   let error () = error_elim_arity env ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = whd_all env !evdref (EConstr.of_constr pt) in
-    match kind_of_term pt', ar with
+    let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+    match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error ();
-        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+        if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
+        srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
     | Evar (ev,_), [] ->
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
-        evdref := Evd.define ev (mkSort s) evd
+        evdref := Evd.define ev (Constr.mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
-        srec (push_rel d env) (lift 1 pt') ar'
+        srec (push_rel d env) (Vars.lift 1 pt') ar'
     | _ ->
         error ()
   in
-  srec env pj.uj_type (List.rev arsign)
+  srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
 
 let e_type_case_branches env evdref (ind,largs) pj c =
   let specif = lookup_mind_specif env (fst ind) in
@@ -128,24 +134,25 @@ let e_judge_of_case env evdref ci pj cj lfj =
     uj_type = rslty }
 
 let check_type_fixpoint loc env evdref lna lar vdefj =
+  let open EConstr in
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
         if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
-		  (EConstr.of_constr (lift lt lar.(i)))) then
+		  (Vars.lift lt lar.(i))) then
           Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
-            i lna vdefj lar
+            i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
       done
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in
+  let pj = Retyping.get_judgment_of env sigma p in
   let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
-    error_elim_arity env ind sorts c pj
+    error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
       (Some(ksort,s,error_elim_explain ksort s))
 
 let e_judge_of_cast env evdref cj k tj =
@@ -160,21 +167,36 @@ let enrich_env env evdref =
   let penv' = Pre_env.({ penv with env_stratification =
     { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
   Environ.env_of_pre_env penv'
+
+let check_fix env sigma pfix =
+  let inj c = EConstr.to_constr sigma c in
+  let (idx, (ids, cs, ts)) = pfix in
+  check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let check_cofix env sigma pcofix =
+  let inj c = EConstr.to_constr sigma c in
+  let (idx, (ids, cs, ts)) = pcofix in
+  check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let make_judge c ty =
+  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
 			  
 (* The typing machine with universes and existential variables. *)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  match kind_of_term cstr with
+  let open EConstr in
+  let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
+  match EConstr.kind !evdref cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = meta_type !evdref n }
+        { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
 
     | Evar ev ->
-	let ty = Evd.existential_type !evdref ev in
-	let jty = execute env evdref (whd_evar !evdref ty) in
+	let ty = EConstr.existential_type !evdref ev in
+	let jty = execute env evdref ty in
 	let jty = e_assumption_of_judgment env evdref jty in
-	{ uj_val = cstr; uj_type = jty }
+	{ uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
 
     | Rel n ->
 	judge_of_relative env n
@@ -183,13 +205,13 @@ let rec execute env evdref cstr =
         judge_of_variable env id
 
     | Const c ->
-        make_judge cstr (rename_type_of_constant env c)
+        make_judge cstr (EConstr.of_constr (rename_type_of_constant env c))
 
     | Ind ind ->
-	make_judge cstr (rename_type_of_inductive env ind)
+	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind))
 
     | Construct cstruct ->
-	make_judge cstr (rename_type_of_constructor env cstruct)
+	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evdref c in
@@ -200,13 +222,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env fix;
+        check_fix env !evdref fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env cofix;
+        check_cofix env !evdref cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
@@ -222,7 +244,7 @@ let rec execute env evdref cstr =
     | App (f,args) ->
         let jl = execute_array env evdref args in
 	let j =
-	  match kind_of_term f with
+	  match EConstr.kind !evdref f with
 	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
@@ -273,7 +295,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let lara = Array.map (e_assumption_of_judgment env evdref) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
-  let vdefv = Array.map j_val vdefj in
+  let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
   let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
@@ -282,8 +304,8 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then
-    error_actual_type env j (nf_evar !evdref t)
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
+    error_actual_type env j (EConstr.to_constr !evdref t)
 
 (* Type of a constr *)
 
@@ -328,4 +350,4 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c)))
+let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
-- 
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.
---
 pretyping/typing.ml | 191 +++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 131 insertions(+), 60 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c948f9b9a7..17adea5f2c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,20 +6,31 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Pp
 open CErrors
 open Util
 open Term
+open EConstr
 open Vars
 open Environ
 open Reductionops
-open Type_errors
 open Inductive
 open Inductiveops
 open Typeops
 open Arguments_renaming
+open Pretype_errors
 open Context.Rel.Declaration
 
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let push_rec_types pfix env =
   let (i, c, t) = pfix in
   let inj c = EConstr.Unsafe.to_constr c in
@@ -31,57 +42,57 @@ let meta_type evd mv =
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
   meta_instance evd ty
 
-let constant_type_knowing_parameters env cst jl =
-  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+let constant_type_knowing_parameters env sigma cst jl =
+  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
   EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
 
-let inductive_type_knowing_parameters env (ind,u) jl =
+let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
-  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
-  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
+  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
-    | _ -> error_not_type env j
+    | _ -> error_not_a_type env !evdref j
 
 let e_assumption_of_judgment env evdref j =
-  try EConstr.of_constr (e_type_judgment env evdref j).utj_val
-  with TypeError _ ->
-    error_assumption env j
+  try (e_type_judgment env evdref j).utj_val
+  with Type_errors.TypeError _ | PretypeError _ ->
+    error_assumption env !evdref j
 
 let e_judge_of_apply env evdref funj argjv =
   let open EConstr in
   let rec apply_rec n typ = function
   | [] ->
-      { uj_val  = Constr.mkApp (j_val funj, Array.map j_val argjv);
-        uj_type = EConstr.Unsafe.to_constr typ }
+      { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
+        uj_type = typ }
   | hj::restjl ->
       match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
-	 if Evarconv.e_cumul env evdref (EConstr.of_constr hj.uj_type) c1 then
-	   apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
+	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
+	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
 	 else
-	   error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
+	   error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
       | Evar ev ->
 	  let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
           evdref := evd';
           let (_,_,c2) = destProd evd' t in
-	  apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
+	  apply_rec (n+1) (subst1 hj.uj_val c2) restjl
       | _ ->
-	  error_cant_apply_not_functional env funj argjv
+	  error_cant_apply_not_functional env !evdref funj argjv
   in
-  apply_rec 1 (EConstr.of_constr funj.uj_type) (Array.to_list argjv)
+  apply_rec 1 funj.uj_type (Array.to_list argjv)
 
 let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
-    error_number_branches env cj (Array.length explft);
+    error_number_branches env !evdref cj (Array.length explft);
   for i = 0 to Array.length explft - 1 do
-    if not (Evarconv.e_cumul env evdref (EConstr.of_constr lfj.(i).uj_type) (EConstr.of_constr explft.(i))) then
-      error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
+    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
+      error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
   done
 
 let max_sort l =
@@ -92,13 +103,13 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let open EConstr in
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
-  let error () = error_elim_arity env ind allowed_sorts c pj None in
+  let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
     let pt' = EConstr.of_constr (whd_all env !evdref pt) in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
-        srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
+        srec (push_rel (local_assum (na1,a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
@@ -106,27 +117,43 @@ let e_is_correct_arity env evdref c pj ind specif params =
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
         evdref := Evd.define ev (Constr.mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
-        srec (push_rel d env) (Vars.lift 1 pt') ar'
+        srec (push_rel d env) (lift 1 pt') ar'
     | _ ->
         error ()
   in
-  srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
+  srec env pj.uj_type (List.rev arsign)
+
+let lambda_applist_assum sigma n c l =
+  let open EConstr in
+  let rec app n subst t l =
+    if Int.equal n 0 then
+      if l == [] then substl subst t
+      else anomaly (Pp.str "Not enough arguments")
+    else match EConstr.kind sigma t, l with
+    | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  app n [] c l
 
 let e_type_case_branches env evdref (ind,largs) pj c =
   let specif = lookup_mind_specif env (fst ind) in
   let nparams = inductive_params specif in
   let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
+  let realargs = List.map EConstr.of_constr realargs in
   let () = e_is_correct_arity env evdref c pj ind specif params in
-  let lc = build_branches_type ind specif params p in
+  let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
+  let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
-  let ty = whd_betaiota !evdref (EConstr.of_constr (lambda_applist_assum (n+1) p (realargs@[c]))) in
+  let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
+  let ty = EConstr.of_constr ty in
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
+  let open EConstr in
   let indspec =
-    try find_mrectype env !evdref (EConstr.of_constr cj.uj_type)
-    with Not_found -> error_case_not_inductive env cj in
+    try find_mrectype env !evdref cj.uj_type
+    with Not_found -> error_case_not_inductive env !evdref cj in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
   e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
@@ -138,27 +165,28 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
-        if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
-		  (Vars.lift lt lar.(i))) then
-          Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
-            i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
+        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
+          error_ill_typed_rec_body ~loc env !evdref
+            i lna vdefj lar
       done
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
+  let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
-    error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
-      (Some(ksort,s,error_elim_explain ksort s))
+    error_elim_arity env sigma ind sorts c pj
+      (Some(ksort,s,Type_errors.error_elim_explain ksort s))
 
 let e_judge_of_cast env evdref cj k tj =
+  let open EConstr in
   let expected_type = tj.utj_val in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr cj.uj_type) (EConstr.of_constr expected_type)) then
-    error_actual_type env cj expected_type;
+  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+    error_actual_type_core env !evdref cj expected_type;
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
 
@@ -178,11 +206,56 @@ let check_cofix env sigma pcofix =
   let (idx, (ids, cs, ts)) = pcofix in
   check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
 
-let make_judge c ty =
-  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
-			  
 (* The typing machine with universes and existential variables. *)
 
+let judge_of_prop =
+  { uj_val = EConstr.mkProp;
+    uj_type = EConstr.mkSort type1_sort }
+
+let judge_of_set =
+  { uj_val = EConstr.mkSet;
+    uj_type = EConstr.mkSort type1_sort }
+
+let judge_of_prop_contents = function
+  | Null -> judge_of_prop
+  | Pos -> judge_of_set
+
+let judge_of_type u =
+  let uu = Univ.Universe.super u in
+    { uj_val = EConstr.mkType u;
+      uj_type = EConstr.mkType uu }
+
+let judge_of_relative env v =
+  Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
+
+let judge_of_variable env id =
+  Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
+
+let judge_of_projection env sigma p cj =
+  let pb = lookup_projection p env in
+  let (ind,u), args =
+    try find_mrectype env sigma cj.uj_type
+    with Not_found -> error_case_not_inductive env sigma cj
+  in
+  let args = List.map EConstr.of_constr args in
+    let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
+    let ty = substl (cj.uj_val :: List.rev args) ty in
+      {uj_val = EConstr.mkProj (p,cj.uj_val);
+       uj_type = ty}
+
+let judge_of_abstraction env name var j =
+  { uj_val = mkLambda (name, var.utj_val, j.uj_val);
+    uj_type = mkProd (name, var.utj_val, j.uj_type) }
+
+let judge_of_product env name t1 t2 =
+  let s = sort_of_product env t1.utj_type t2.utj_type in
+  { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
+    uj_type = mkSort s }
+
+let judge_of_letin env name defj typj j =
+  { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
+    uj_type = subst1 defj.uj_val j.uj_type }
+
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
@@ -190,13 +263,13 @@ let rec execute env evdref cstr =
   let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
   match EConstr.kind !evdref cstr with
     | Meta n ->
-        { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
+        { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) }
 
     | Evar ev ->
 	let ty = EConstr.existential_type !evdref ev in
 	let jty = execute env evdref ty in
 	let jty = e_assumption_of_judgment env evdref jty in
-	{ uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
+	{ uj_val = cstr; uj_type = jty }
 
     | Rel n ->
 	judge_of_relative env n
@@ -239,7 +312,7 @@ let rec execute env evdref cstr =
 
     | Proj (p, c) -> 
         let cj = execute env evdref c in
-	  judge_of_projection env p (Evarutil.j_nf_evar !evdref cj)
+	  judge_of_projection env !evdref p cj
 
     | App (f,args) ->
         let jl = execute_array env evdref args in
@@ -248,13 +321,11 @@ let rec execute env evdref cstr =
 	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (inductive_type_knowing_parameters env ind
-		    (Evarutil.jv_nf_evar !evdref jl))
+		  (inductive_type_knowing_parameters env !evdref ind jl)
 	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (constant_type_knowing_parameters env cst
-		    (Evarutil.jv_nf_evar !evdref jl))
+		  (constant_type_knowing_parameters env !evdref cst jl)
 	    | _ ->
 		execute env evdref f
 	in
@@ -263,14 +334,14 @@ let rec execute env evdref cstr =
     | Lambda (name,c1,c2) ->
         let j = execute env evdref c1 in
 	let var = e_type_judgment env evdref j in
-	let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
+	let env1 = push_rel (local_assum (name, var.utj_val)) env in
         let j' = execute env1 evdref c2 in
         judge_of_abstraction env1 name var j'
 
     | Prod (name,c1,c2) ->
         let j = execute env evdref c1 in
         let varj = e_type_judgment env evdref j in
-	let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
+	let env1 = push_rel (local_assum (name, varj.utj_val)) env in
         let j' = execute env1 evdref c2 in
         let varj' = e_type_judgment env1 evdref j' in
 	judge_of_product env name varj varj'
@@ -280,7 +351,7 @@ let rec execute env evdref cstr =
         let j2 = execute env evdref c2 in
         let j2 = e_type_judgment env evdref j2 in
         let _ =  e_judge_of_cast env evdref j1 DEFAULTcast j2 in
-        let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
+        let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in
         let j3 = execute env1 evdref c3 in
         judge_of_letin env name j1 j2 j3
 
@@ -295,7 +366,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let lara = Array.map (e_assumption_of_judgment env evdref) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
-  let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
+  let vdefv = Array.map j_val vdefj in
   let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
@@ -304,8 +375,8 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
-    error_actual_type env j (EConstr.to_constr !evdref t)
+  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+    error_actual_type_core env !evdref j t
 
 (* Type of a constr *)
 
@@ -313,7 +384,7 @@ let unsafe_type_of env evd c =
   let evdref = ref evd in
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-    j.uj_type
+    EConstr.Unsafe.to_constr j.uj_type
 
 (* Sort of a type *)
 
@@ -331,23 +402,23 @@ let type_of ?(refresh=false) env evd c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type)
-    else !evdref, j.uj_type
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
+    else !evdref, EConstr.Unsafe.to_constr j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) in
+      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
       let () = evdref := evd in
       c
-    else j.uj_type
+    else EConstr.Unsafe.to_constr j.uj_type
 
 let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  nf_evar !evdref c
+  nf_evar !evdref (EConstr.Unsafe.to_constr c)
 
 let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
-- 
cgit v1.2.3


From 536026f3e20f761e8ef366ed732da7d3b626ac5e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 15:39:01 +0100
Subject: Cleaning up opening of the EConstr module in pretyping folder.

---
 pretyping/typing.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 17adea5f2c..cf58a0b668 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -65,7 +65,6 @@ let e_assumption_of_judgment env evdref j =
     error_assumption env !evdref j
 
 let e_judge_of_apply env evdref funj argjv =
-  let open EConstr in
   let rec apply_rec n typ = function
   | [] ->
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
@@ -100,7 +99,6 @@ let max_sort l =
   if Sorts.List.mem InSet l then InSet else InProp
 
 let e_is_correct_arity env evdref c pj ind specif params =
-  let open EConstr in
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
@@ -124,7 +122,6 @@ let e_is_correct_arity env evdref c pj ind specif params =
   srec env pj.uj_type (List.rev arsign)
 
 let lambda_applist_assum sigma n c l =
-  let open EConstr in
   let rec app n subst t l =
     if Int.equal n 0 then
       if l == [] then substl subst t
@@ -150,7 +147,6 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
-  let open EConstr in
   let indspec =
     try find_mrectype env !evdref cj.uj_type
     with Not_found -> error_case_not_inductive env !evdref cj in
@@ -161,7 +157,6 @@ let e_judge_of_case env evdref ci pj cj lfj =
     uj_type = rslty }
 
 let check_type_fixpoint loc env evdref lna lar vdefj =
-  let open EConstr in
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
@@ -183,7 +178,6 @@ let check_allowed_sort env sigma ind c p =
       (Some(ksort,s,Type_errors.error_elim_explain ksort s))
 
 let e_judge_of_cast env evdref cj k tj =
-  let open EConstr in
   let expected_type = tj.utj_val in
   if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
     error_actual_type_core env !evdref cj expected_type;
@@ -259,7 +253,6 @@ let judge_of_letin env name defj typj j =
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  let open EConstr in
   let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
   match EConstr.kind !evdref cstr with
     | Meta n ->
-- 
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.

---
 pretyping/typing.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cf58a0b668..29697260f7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -40,6 +40,7 @@ let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
+  let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
 let constant_type_knowing_parameters env sigma cst jl =
@@ -256,7 +257,7 @@ let rec execute env evdref cstr =
   let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
   match EConstr.kind !evdref cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) }
+        { uj_val = cstr; uj_type = meta_type !evdref n }
 
     | Evar ev ->
 	let ty = EConstr.existential_type !evdref ev in
-- 
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/typing.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 29697260f7..40ef2450a3 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -138,7 +138,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let nparams = inductive_params specif in
   let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
-  let realargs = List.map EConstr.of_constr realargs in
+  let params = List.map EConstr.Unsafe.to_constr params in
   let () = e_is_correct_arity env evdref c pj ind specif params in
   let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
   let lc = Array.map EConstr.of_constr lc in
@@ -232,7 +232,6 @@ let judge_of_projection env sigma p cj =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj
   in
-  let args = List.map EConstr.of_constr args in
     let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
     let ty = substl (cj.uj_val :: List.rev args) ty in
       {uj_val = EConstr.mkProj (p,cj.uj_val);
-- 
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/typing.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 40ef2450a3..f67e0bddc7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -53,7 +53,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
-  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with
+  match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -71,7 +71,7 @@ let e_judge_of_apply env evdref funj argjv =
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
         uj_type = typ }
   | hj::restjl ->
-      match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
+      match EConstr.kind !evdref (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
 	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -104,7 +104,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+    let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
@@ -144,7 +144,6 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
   let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
-  let ty = EConstr.of_constr ty in
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
-- 
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

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

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f67e0bddc7..d24160ea54 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -395,7 +395,7 @@ let type_of ?(refresh=false) env evd c =
   (* side-effect on evdref *)
     if refresh then
       Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
-    else !evdref, EConstr.Unsafe.to_constr j.uj_type
+    else !evdref, j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
   let env = enrich_env env evdref in
@@ -405,7 +405,7 @@ let e_type_of ?(refresh=false) env evdref c =
       let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
       let () = evdref := evd in
       c
-    else EConstr.Unsafe.to_constr j.uj_type
+    else j.uj_type
 
 let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
-- 
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.

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

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d24160ea54..7baff421fb 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -376,7 +376,7 @@ let unsafe_type_of env evd c =
   let evdref = ref evd in
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-    EConstr.Unsafe.to_constr j.uj_type
+    j.uj_type
 
 (* Sort of a type *)
 
@@ -411,6 +411,6 @@ let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  nf_evar !evdref (EConstr.Unsafe.to_constr c)
+  EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c))
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
+let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
-- 
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.

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

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7baff421fb..e6f1e46b6d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -252,7 +252,7 @@ let judge_of_letin env name defj typj j =
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
+  let cstr = whd_evar !evdref cstr in
   match EConstr.kind !evdref cstr with
     | Meta n ->
         { uj_val = cstr; uj_type = meta_type !evdref n }
@@ -411,6 +411,6 @@ let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c))
+  nf_evar !evdref c
 
 let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
-- 
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/typing.ml | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e6f1e46b6d..bdd3663d1a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -12,9 +12,9 @@ open Pp
 open CErrors
 open Util
 open Term
+open Environ
 open EConstr
 open Vars
-open Environ
 open Reductionops
 open Inductive
 open Inductiveops
@@ -23,14 +23,6 @@ open Arguments_renaming
 open Pretype_errors
 open Context.Rel.Declaration
 
-let local_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let push_rec_types pfix env =
   let (i, c, t) = pfix in
   let inj c = EConstr.Unsafe.to_constr c in
@@ -101,14 +93,15 @@ let max_sort l =
 
 let e_is_correct_arity env evdref c pj ind specif params =
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
+  let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
     let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
-        srec (push_rel (local_assum (na1,a1)) env) t ar'
+        if not (Evarconv.e_cumul env evdref a1 a1') then error ();
+        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
@@ -326,14 +319,14 @@ let rec execute env evdref cstr =
     | Lambda (name,c1,c2) ->
         let j = execute env evdref c1 in
 	let var = e_type_judgment env evdref j in
-	let env1 = push_rel (local_assum (name, var.utj_val)) env in
+	let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
         let j' = execute env1 evdref c2 in
         judge_of_abstraction env1 name var j'
 
     | Prod (name,c1,c2) ->
         let j = execute env evdref c1 in
         let varj = e_type_judgment env evdref j in
-	let env1 = push_rel (local_assum (name, varj.utj_val)) env in
+	let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
         let j' = execute env1 evdref c2 in
         let varj' = e_type_judgment env1 evdref j' in
 	judge_of_product env name varj varj'
@@ -343,7 +336,7 @@ let rec execute env evdref cstr =
         let j2 = execute env evdref c2 in
         let j2 = e_type_judgment env evdref j2 in
         let _ =  e_judge_of_cast env evdref j1 DEFAULTcast j2 in
-        let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in
+        let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
         let j3 = execute env1 evdref c3 in
         judge_of_letin env name j1 j2 j3
 
-- 
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/typing.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bdd3663d1a..dec22ecd00 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -92,8 +92,7 @@ let max_sort l =
   if Sorts.List.mem InSet l then InSet else InProp
 
 let e_is_correct_arity env evdref c pj ind specif params =
-  let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
-  let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
+  let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
-- 
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/typing.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index dec22ecd00..d9d64e7eb3 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -46,7 +46,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
 
 let e_type_judgment env evdref j =
   match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
-    | Sort s -> {utj_val = j.uj_val; utj_type = s }
+    | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
@@ -102,6 +102,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
         if not (Evarconv.e_cumul env evdref a1 a1') then error ();
         srec (push_rel (LocalAssum (na1,a1)) env) t ar'
     | Sort s, [] ->
+        let s = ESorts.kind !evdref s in
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
     | Evar (ev,_), [] ->
@@ -161,7 +162,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
+  let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
@@ -288,11 +289,13 @@ let rec execute env evdref cstr =
         check_cofix env !evdref cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
-    | Sort (Prop c) ->
-	judge_of_prop_contents c
-
-    | Sort (Type u) ->
+    | Sort s ->
+      begin match ESorts.kind !evdref s with
+      | Prop c ->
+        judge_of_prop_contents c
+      | Type u ->
         judge_of_type u
+      end
 
     | Proj (p, c) -> 
         let cj = execute env evdref c in
-- 
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/typing.ml | 33 ++++++++++++++++++++-------------
 1 file changed, 20 insertions(+), 13 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d9d64e7eb3..c2a030bcd2 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,11 +35,13 @@ let meta_type evd mv =
   let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
-let constant_type_knowing_parameters env sigma cst jl =
+let constant_type_knowing_parameters env sigma (cst, u) jl =
+  let u = Unsafe.to_instance u in
   let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
-  EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
+  EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp)
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
+  let u = Unsafe.to_instance u in
   let mspec = lookup_mind_specif env ind in
   let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
@@ -140,9 +142,10 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
-  let indspec =
+  let ((ind, u), spec) =
     try find_mrectype env !evdref cj.uj_type
     with Not_found -> error_case_not_inductive env !evdref cj in
+  let indspec = ((ind, EInstance.kind !evdref u), spec) in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
   e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
@@ -224,6 +227,7 @@ let judge_of_projection env sigma p cj =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj
   in
+  let u = EInstance.kind sigma u in
     let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
     let ty = substl (cj.uj_val :: List.rev args) ty in
       {uj_val = EConstr.mkProj (p,cj.uj_val);
@@ -262,14 +266,17 @@ let rec execute env evdref cstr =
     | Var id ->
         judge_of_variable env id
 
-    | Const c ->
-        make_judge cstr (EConstr.of_constr (rename_type_of_constant env c))
+    | Const (c, u) ->
+        let u = EInstance.kind !evdref u in
+        make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
 
-    | Ind ind ->
-	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind))
+    | Ind (ind, u) ->
+        let u = EInstance.kind !evdref u in
+	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
 
-    | Construct cstruct ->
-	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct))
+    | Construct (cstruct, u) ->
+        let u = EInstance.kind !evdref u in
+	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evdref c in
@@ -305,14 +312,14 @@ let rec execute env evdref cstr =
         let jl = execute_array env evdref args in
 	let j =
 	  match EConstr.kind !evdref f with
-	    | Ind ind when Environ.template_polymorphic_pind ind env ->
+	    | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (inductive_type_knowing_parameters env !evdref ind jl)
-	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
+		  (inductive_type_knowing_parameters env !evdref (ind, u) jl)
+	    | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (constant_type_knowing_parameters env !evdref cst jl)
+		  (constant_type_knowing_parameters env !evdref (cst, u) jl)
 	    | _ ->
 		execute env evdref f
 	in
-- 
cgit v1.2.3