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.

---
 engine/termops.ml | 303 ++++++++++++++++++++++++++++--------------------------
 1 file changed, 159 insertions(+), 144 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 35917b368f..356312e2f6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -236,35 +236,35 @@ let it_mkLambda_or_LetIn_from_no_LetIn c decls =
 (* *)
 
 (* strips head casts and flattens head applications *)
-let rec strip_head_cast c = match kind_of_term c with
+let rec strip_head_cast sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
-      let rec collapse_rec f cl2 = match kind_of_term f with
+      let rec collapse_rec f cl2 = match EConstr.kind sigma f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| Cast (c,_,_) -> collapse_rec c cl2
-	| _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2)
+	| _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2)
       in
       collapse_rec f cl
-  | Cast (c,_,_) -> strip_head_cast c
+  | Cast (c,_,_) -> strip_head_cast sigma c
   | _ -> c
 
-let rec drop_extra_implicit_args c = match kind_of_term c with
+let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
   (* Removed trailing extra implicit arguments, what improves compatibility
      for constants with recently added maximal implicit arguments *)
-  | App (f,args) when isEvar (Array.last args) ->
-      drop_extra_implicit_args
-	(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
-  | _ -> c
+  | App (f,args) when EConstr.isEvar sigma (Array.last args) ->
+      drop_extra_implicit_args sigma
+	(EConstr.mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+  | _ -> EConstr.Unsafe.to_constr c
 
 (* Get the last arg of an application *)
-let last_arg c = match kind_of_term c with
-  | App (f,cl) -> Array.last cl
+let last_arg sigma c = match EConstr.kind sigma c with
+  | App (f,cl) -> EConstr.Unsafe.to_constr (Array.last cl)
   | _ -> anomaly (Pp.str "last_arg")
 
 (* Get the last arg of an application *)
-let decompose_app_vect c =
-  match kind_of_term c with
-  | App (f,cl) -> (f, cl)
-  | _ -> (c,[||])
+let decompose_app_vect sigma c =
+  match EConstr.kind sigma c with
+  | App (f,cl) -> (EConstr.Unsafe.to_constr f, Array.map EConstr.Unsafe.to_constr cl)
+  | _ -> (EConstr.Unsafe.to_constr c,[||])
 
 let adjust_app_list_size f1 l1 f2 l2 =
   let len1 = List.length l1 and len2 = List.length l2 in
@@ -400,9 +400,11 @@ let map_constr_with_binders_left_to_right g f l c =
 	else mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
-let map_constr_with_full_binders g f l cstr =
+let map_constr_with_full_binders sigma g f l cstr =
+  let inj c = EConstr.Unsafe.to_constr c in
+  let open EConstr in
   let open RelDecl in
-  match kind_of_term cstr with
+  match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> cstr
   | Cast (c,k, t) ->
@@ -411,16 +413,16 @@ let map_constr_with_full_binders g f l cstr =
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na,t)) l) c in
+      let c' = f (g (LocalAssum (na, inj t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na,t)) l) c in
+      let c' = f (g (LocalAssum (na, inj t)) l) c in
       if t==t' && c==c' then cstr else  mkLambda (na, t', c')
   | LetIn (na,b,t,c) ->
       let b' = f l b in
       let t' = f l t in
-      let c' = f (g (LocalDef (na,b,t)) l) c in
+      let c' = f (g (LocalDef (na, inj b, inj t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -441,7 +443,7 @@ let map_constr_with_full_binders g f l cstr =
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -449,7 +451,7 @@ let map_constr_with_full_binders g f l cstr =
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -462,30 +464,31 @@ let map_constr_with_full_binders g f l cstr =
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_full_binders g f n acc c =
+let fold_constr_with_full_binders sigma g f n acc c =
   let open RelDecl in
-  match kind_of_term c with
+  let inj c = EConstr.Unsafe.to_constr c in
+  match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
-let fold_constr_with_binders g f n acc c =
-  fold_constr_with_full_binders (fun _ x -> g x) f n acc c
+let fold_constr_with_binders sigma g f n acc c =
+  fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c
 
 (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
    subterms of [c]; it carries an extra data [acc] which is processed by [g] at
@@ -520,29 +523,29 @@ let iter_constr_with_full_binders g f l c =
 
 exception Occur
 
-let occur_meta c =
-  let rec occrec c = match kind_of_term c with
+let occur_meta sigma c =
+  let rec occrec c = match EConstr.kind sigma c with
     | Meta _ -> raise Occur
-    | _ -> iter_constr occrec c
+    | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
-let occur_existential c =
-  let rec occrec c = match kind_of_term c with
+let occur_existential sigma c =
+  let rec occrec c = match EConstr.kind sigma c with
     | Evar _ -> raise Occur
-    | _ -> iter_constr occrec c
+    | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
-let occur_meta_or_existential c =
-  let rec occrec c = match kind_of_term c with
+let occur_meta_or_existential sigma c =
+  let rec occrec c = match EConstr.kind sigma c with
     | Evar _ -> raise Occur
     | Meta _ -> raise Occur
-    | _ -> iter_constr occrec c
+    | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
-let occur_evar n c =
-  let rec occur_rec c = match kind_of_term c with
+let occur_evar sigma n c =
+  let rec occur_rec c = match EConstr.kind sigma c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
-    | _ -> iter_constr occur_rec c
+    | _ -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
@@ -550,55 +553,55 @@ let occur_in_global env id constr =
   let vars = vars_of_global env constr in
   if Id.Set.mem id vars then raise Occur
 
-let occur_var env id c =
+let occur_var env sigma id c =
   let rec occur_rec c =
-    match kind_of_term c with
-    | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c
-    | _ -> iter_constr occur_rec c
+    match EConstr.kind sigma c with
+    | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
+    | _ -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
-let occur_var_in_decl env hyp decl =
+let occur_var_in_decl env sigma hyp decl =
   let open NamedDecl in
   match decl with
-    | LocalAssum (_,typ) -> occur_var env hyp typ
+    | LocalAssum (_,typ) -> occur_var env sigma hyp (EConstr.of_constr typ)
     | LocalDef (_, body, typ) ->
-        occur_var env hyp typ ||
-        occur_var env hyp body
+        occur_var env sigma hyp (EConstr.of_constr typ) ||
+        occur_var env sigma hyp (EConstr.of_constr body)
 
-let local_occur_var id c =
-  let rec occur c = match kind_of_term c with
+let local_occur_var sigma id c =
+  let rec occur c = match EConstr.kind sigma c with
   | Var id' -> if Id.equal id id' then raise Occur
-  | _ -> Constr.iter occur c
+  | _ -> EConstr.iter sigma occur c
   in
   try occur c; false with Occur -> true
 
   (* returns the list of free debruijn indices in a term *)
 
-let free_rels m =
-  let rec frec depth acc c = match kind_of_term c with
+let free_rels sigma m =
+  let rec frec depth acc c = match EConstr.kind sigma c with
     | Rel n       -> if n >= depth then Int.Set.add (n-depth+1) acc else acc
-    | _ -> fold_constr_with_binders succ frec depth acc c
+    | _ -> fold_constr_with_binders sigma succ frec depth acc c
   in
   frec 1 Int.Set.empty m
 
 (* collects all metavar occurrences, in left-to-right order, preserving
  * repetitions and all. *)
 
-let collect_metas c =
+let collect_metas sigma c =
   let rec collrec acc c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
       | Meta mv -> List.add_set Int.equal mv acc
-      | _       -> fold_constr collrec acc c
+      | _       -> EConstr.fold sigma collrec acc c
   in
   List.rev (collrec [] c)
 
 (* collects all vars; warning: this is only visible vars, not dependencies in
    all section variables; for the latter, use global_vars_set *)
-let collect_vars c =
-  let rec aux vars c = match kind_of_term c with
+let collect_vars sigma c =
+  let rec aux vars c = match EConstr.kind sigma c with
   | Var id -> Id.Set.add id vars
-  | _ -> fold_constr aux vars c in
+  | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
 let vars_of_global_reference env gr =
@@ -608,54 +611,54 @@ let vars_of_global_reference env gr =
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
-let dependent_main noevar univs m t =
+let dependent_main noevar univs sigma m t =
   let eqc x y =
-    if univs then not (Option.is_empty (Universes.eq_constr_universes x y))
-    else eq_constr_nounivs x y
+    if univs then not (Option.is_empty (EConstr.eq_constr_universes sigma x y))
+    else EConstr.eq_constr_nounivs sigma x y
   in
   let rec deprec m t =
     if eqc m t then
       raise Occur
     else
-      match kind_of_term m, kind_of_term t with
+      match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    deprec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm)));
 	    CArray.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when noevar && isMeta c -> ()
+	| _, Cast (c,_,_) when noevar && EConstr.isMeta sigma c -> ()
 	| _, Evar _ when noevar -> ()
-	| _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t
+	| _ -> EConstr.iter_with_binders sigma (fun c -> EConstr.Vars.lift 1 c) deprec m t
   in
   try deprec m t; false with Occur -> true
 
-let dependent = dependent_main false false
-let dependent_no_evar = dependent_main true false
+let dependent sigma c t = dependent_main false false sigma c t
+let dependent_no_evar sigma c t = dependent_main true false sigma c t
 
-let dependent_univs = dependent_main false true
-let dependent_univs_no_evar = dependent_main true true
+let dependent_univs sigma c t = dependent_main false true sigma c t
+let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t
 
-let dependent_in_decl a decl =
+let dependent_in_decl sigma a decl =
   let open NamedDecl in
   match decl with
-    | LocalAssum (_,t) -> dependent a t
-    | LocalDef (_, body, t) -> dependent a body || dependent a t
+    | LocalAssum (_,t) -> dependent sigma a (EConstr.of_constr t)
+    | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t)
 
-let count_occurrences m t =
+let count_occurrences sigma m t =
   let n = ref 0 in
   let rec countrec m t =
-    if eq_constr m t then
+    if EConstr.eq_constr sigma m t then
       incr n
     else
-      match kind_of_term m, kind_of_term t with
+      match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    countrec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm)));
 	    Array.iter (countrec m)
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when isMeta c -> ()
+	| _, Cast (c,_,_) when EConstr.isMeta sigma c -> ()
 	| _, Evar _ -> ()
-	| _ -> iter_constr_with_binders (lift 1) countrec m t
+	| _ -> EConstr.iter_with_binders sigma (EConstr.Vars.lift 1) countrec m t
   in
   countrec m t;
   !n
@@ -663,7 +666,7 @@ let count_occurrences m t =
 (* Synonymous *)
 let occur_term = dependent
 
-let pop t = lift (-1) t
+let pop t = EConstr.Unsafe.to_constr (EConstr.Vars.lift (-1) t)
 
 (***************************)
 (*  bindings functions *)
@@ -678,45 +681,45 @@ let rec subst_meta bl c =
     | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
     | _ -> map_constr (subst_meta bl) c
 
-let rec strip_outer_cast c = match kind_of_term c with
-  | Cast (c,_,_) -> strip_outer_cast c
-  | _ -> c
+let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
+  | Cast (c,_,_) -> strip_outer_cast sigma c
+  | _ -> EConstr.Unsafe.to_constr c
 
 (* flattens application lists throwing casts in-between *)
-let collapse_appl c = match kind_of_term c with
+let collapse_appl sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
-        match kind_of_term (strip_outer_cast f) with
+        match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma f)) with
         | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-        | _ -> mkApp (f,cl2)
+        | _ -> EConstr.mkApp (f,cl2)
       in
-      collapse_rec f cl
-  | _ -> c
+      EConstr.Unsafe.to_constr (collapse_rec f cl)
+  | _ -> EConstr.Unsafe.to_constr c
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
-let prefix_application eq_fun (k,c) (t : constr) =
-  let c' = collapse_appl c and t' = collapse_appl t in
-  match kind_of_term c', kind_of_term t' with
+let prefix_application sigma eq_fun (k,c) t =
+  let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in
+  match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+	   && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (EConstr.mkApp (EConstr.mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else
 	  None
     | _ -> None
 
-let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
-  let c' = collapse_appl c and t' = collapse_appl t in
-  match kind_of_term c', kind_of_term t' with
+let my_prefix_application sigma eq_fun (k,c) by_c t =
+  let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in
+  match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+	   && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (EConstr.mkApp ((EConstr.Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
 	else
 	  None
     | _ -> None
@@ -725,35 +728,35 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
    substitutes [(Rel 1)] for all occurrences of term [c] in a term [t];
    works if [c] has rels *)
 
-let subst_term_gen eq_fun c t =
+let subst_term_gen sigma eq_fun c t =
   let rec substrec (k,c as kc) t =
-    match prefix_application eq_fun kc t with
+    match prefix_application sigma eq_fun kc t with
       | Some x -> x
       | None ->
-    if eq_fun c t then mkRel k
+    if eq_fun sigma c t then EConstr.mkRel k
     else
-      map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
+      EConstr.map_with_binders sigma (fun (k,c) -> (k+1, EConstr.Vars.lift 1 c)) substrec kc t
   in
-  substrec (1,c) t
+  EConstr.Unsafe.to_constr (substrec (1,c) t)
 
-let subst_term = subst_term_gen eq_constr
+let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t
 
 (* Recognizing occurrences of a given subterm in a term :
    [replace_term c1 c2 t] substitutes [c2] for all occurrences of
    term [c1] in a term [t]; works if [c1] and [c2] have rels *)
 
-let replace_term_gen eq_fun c by_c in_t =
+let replace_term_gen sigma eq_fun c by_c in_t =
   let rec substrec (k,c as kc) t =
-    match my_prefix_application eq_fun kc by_c t with
+    match my_prefix_application sigma eq_fun kc by_c t with
       | Some x -> x
       | None ->
-    (if eq_fun c t then (lift k by_c) else
-      map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c))
+    (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else
+      EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
 	substrec kc t)
   in
-  substrec (0,c) in_t
+  EConstr.Unsafe.to_constr (substrec (0,c) in_t)
 
-let replace_term = replace_term_gen eq_constr
+let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t
 
 let vars_of_env env =
   let s =
@@ -804,13 +807,13 @@ let is_section_variable id =
   try let _ = Global.lookup_named id in true
   with Not_found -> false
 
-let isGlobalRef c =
-  match kind_of_term c with
+let isGlobalRef sigma c =
+  match EConstr.kind sigma c with
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
-let is_template_polymorphic env f =
-  match kind_of_term f with
+let is_template_polymorphic env sigma f =
+  match EConstr.kind sigma f with
   | Ind ind -> Environ.template_polymorphic_pind ind env
   | Const c -> Environ.template_polymorphic_pconstant c env
   | _ -> false
@@ -882,45 +885,46 @@ let filtering env cv_pb c1 c2 =
   in
   aux env cv_pb c1 c2; !evm
 
-let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
-  let rec prodec_rec i l c = match kind_of_term c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
-    | Cast (c,_,_)    -> prodec_rec i l c
-    | _               -> i,l,c in
-  prodec_rec 0 []
+let decompose_prod_letin sigma c =
+  let inj c = EConstr.Unsafe.to_constr c in
+  let rec prodec_rec i l sigma c = match EConstr.kind sigma c with
+    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n, inj t)::l) sigma c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n, inj d, inj t)::l) sigma c
+    | Cast (c,_,_)    -> prodec_rec i l sigma c
+    | _               -> i,l, inj c in
+  prodec_rec 0 [] sigma c
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
-let nb_lam =
-  let rec nbrec n c = match kind_of_term c with
+let nb_lam sigma c =
+  let rec nbrec n c = match EConstr.kind sigma c with
     | Lambda (_,_,c) -> nbrec (n+1) c
     | Cast (c,_,_) -> nbrec n c
     | _ -> n
   in
-  nbrec 0
+  nbrec 0 c
 
 (* similar to nb_lam, but gives the number of products instead *)
-let nb_prod =
-  let rec nbrec n c = match kind_of_term c with
+let nb_prod sigma c =
+  let rec nbrec n c = match EConstr.kind sigma c with
     | Prod (_,_,c) -> nbrec (n+1) c
     | Cast (c,_,_) -> nbrec n c
     | _ -> n
   in
-  nbrec 0
+  nbrec 0 c
 
-let nb_prod_modulo_zeta x =
+let nb_prod_modulo_zeta sigma x =
   let rec count n c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
         Prod(_,_,t) -> count (n+1) t
-      | LetIn(_,a,_,t) -> count n (subst1 a t)
+      | LetIn(_,a,_,t) -> count n (EConstr.Vars.subst1 a t)
       | Cast(c,_,_) -> count n c
       | _ -> n
   in count 0 x
 
-let align_prod_letin c a : Context.Rel.t * constr =
-  let (lc,_,_) = decompose_prod_letin c in
-  let (la,l,a) = decompose_prod_letin a in
+let align_prod_letin sigma c a : Context.Rel.t * constr =
+  let (lc,_,_) = decompose_prod_letin sigma c in
+  let (la,l,a) = decompose_prod_letin sigma a in
   if not (la >= lc) then invalid_arg "align_prod_letin";
   let (l1,l2) = Util.List.chop lc l in
   l2,it_mkProd_or_LetIn a l1
@@ -1031,22 +1035,33 @@ let clear_named_body id env =
   | d -> push_named d in
   fold_named_context aux env ~init:(reset_context env)
 
-let global_vars env ids = Id.Set.elements (global_vars_set env ids)
+let global_vars_set env sigma constr =
+  let rec filtrec acc c =
+    let acc = match EConstr.kind sigma c with
+    | Var _ | Const _ | Ind _ | Construct _ ->
+      Id.Set.union (vars_of_global env (EConstr.Unsafe.to_constr c)) acc
+    | _ -> acc
+    in
+    EConstr.fold sigma filtrec acc c
+  in
+  filtrec Id.Set.empty constr
+
+let global_vars env sigma ids = Id.Set.elements (global_vars_set env sigma ids)
 
-let global_vars_set_of_decl env = function
-  | NamedDecl.LocalAssum (_,t) -> global_vars_set env t
+let global_vars_set_of_decl env sigma = function
+  | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma (EConstr.of_constr t)
   | NamedDecl.LocalDef (_,c,t) ->
-      Id.Set.union (global_vars_set env t)
-        (global_vars_set env c)
+      Id.Set.union (global_vars_set env sigma (EConstr.of_constr t))
+        (global_vars_set env sigma (EConstr.of_constr c))
 
-let dependency_closure env sign hyps =
+let dependency_closure env sigma sign hyps =
   if Id.Set.is_empty hyps then [] else
     let (_,lh) =
       Context.Named.fold_inside
         (fun (hs,hl) d ->
           let x = NamedDecl.get_id d in
           if Id.Set.mem x hs then
-            (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
+            (Id.Set.union (global_vars_set_of_decl env sigma d) (Id.Set.remove x hs),
             x::hl)
           else (hs,hl))
         ~init:(hyps,[])
-- 
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.

---
 engine/termops.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 356312e2f6..26b22be4e4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1068,6 +1068,17 @@ let dependency_closure env sigma sign hyps =
         sign in
     List.rev lh
 
+let global_app_of_constr sigma c =
+  let open Univ in
+  let open Globnames in
+  match EConstr.kind sigma c with
+  | Const (c, u) -> (ConstRef c, u), None
+  | Ind (i, u) -> (IndRef i, u), None
+  | Construct (c, u) -> (ConstructRef c, u), None
+  | Var id -> (VarRef id, Instance.empty), None
+  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
+  | _ -> raise Not_found
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
-- 
cgit v1.2.3


From b77579ac873975a15978c5a4ecf312d577746d26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 21:59:18 +0100
Subject: Tacred API using EConstr.

---
 engine/termops.ml | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 26b22be4e4..f191e2dc12 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -320,8 +320,19 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    time being almost those of the ML representation (except for
    (co-)fixpoint) *)
 
+let local_assum (na, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let fold_rec_types g (lna,typarray,_) e =
-  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
+  let open EConstr in
+  let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -336,9 +347,9 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right g f l c =
-  let open RelDecl in
-  match kind_of_term c with
+let map_constr_with_binders_left_to_right sigma g f l c =
+  let open EConstr in
+  match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) -> 
@@ -348,18 +359,18 @@ let map_constr_with_binders_left_to_right g f l c =
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (LocalAssum (na,t)) l) b in
+      let b' = f (g (local_assum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (LocalAssum (na,t)) l) b in
+      let b' = f (g (local_assum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (LocalDef (na,bo,t)) l) b in
+      let b' = f (g (local_def (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
-- 
cgit v1.2.3


From 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Nov 2016 13:27:16 +0100
Subject: Typeclasses API using EConstr.

---
 engine/termops.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index f191e2dc12..e5db3c085b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -818,6 +818,15 @@ let is_section_variable id =
   try let _ = Global.lookup_named id in true
   with Not_found -> false
 
+let global_of_constr sigma c =
+  let open Globnames in
+  match EConstr.kind sigma c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, Univ.Instance.empty
+  | _ -> raise Not_found
+
 let isGlobalRef sigma c =
   match EConstr.kind sigma c with
   | Const _ | Ind _ | Construct _ | Var _ -> true
-- 
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.

---
 engine/termops.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index e5db3c085b..16e2c04c8b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -207,10 +207,11 @@ let mkProd_or_LetIn decl c =
 
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
 let mkProd_wo_LetIn decl c =
+  let open EConstr in
   let open RelDecl in
   match decl with
-    | LocalAssum (na,t) -> mkProd (na, t, c)
-    | LocalDef (_,b,_) -> subst1 b c
+    | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c)
+    | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
@@ -1099,6 +1100,15 @@ let global_app_of_constr sigma c =
   | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
   | _ -> raise Not_found
 
+let prod_applist sigma c l =
+  let open EConstr in
+  let rec app subst c l =
+    match EConstr.kind sigma c, l with
+    | Prod(_,_,c), arg::l -> app (arg::subst) c l
+    | _, [] -> Vars.substl subst c
+    | _ -> anomaly (Pp.str "Not enough prod's") in
+  app [] c l
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
-- 
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.

---
 engine/termops.ml | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 16e2c04c8b..c1198e05aa 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -164,9 +164,19 @@ let rel_list n m =
   in
   reln [] 1
 
+let local_assum (na, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let push_rel_assum (x,t) env =
   let open RelDecl in
-  push_rel (LocalAssum (x,t)) env
+  push_rel (local_assum (x,t)) env
 
 let push_rels_assum assums =
   let open RelDecl in
@@ -278,14 +288,15 @@ let adjust_app_list_size f1 l1 f2 l2 =
     (applist (f1,extras), restl1, f2, l2)
 
 let adjust_app_array_size f1 l1 f2 l2 =
+  let open EConstr in
   let len1 = Array.length l1 and len2 = Array.length l2 in
   if Int.equal len1 len2 then (f1,l1,f2,l2)
   else if len1 < len2 then
     let extras,restl2 = Array.chop (len2-len1) l2 in
-    (f1, l1, appvect (f2,extras), restl2)
+    (f1, l1, mkApp (f2,extras), restl2)
   else
     let extras,restl1 = Array.chop (len1-len2) l1 in
-    (appvect (f1,extras), restl1, f2, l2)
+    (mkApp (f1,extras), restl1, f2, l2)
 
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
    subterms of [c]; it carries an extra data [l] (typically a name
@@ -321,16 +332,6 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    time being almost those of the ML representation (except for
    (co-)fixpoint) *)
 
-let local_assum (na, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let fold_rec_types g (lna,typarray,_) e =
   let open EConstr in
   let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in
-- 
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.
---
 engine/termops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index c1198e05aa..83f07d2c62 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1141,6 +1141,7 @@ let impossible_default_case = ref None
 let set_impossible_default_clause c = impossible_default_case := Some c
 
 let coq_unit_judge =
+  let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
   let na1 = Name (Id.of_string "A") in
   let na2 = Name (Id.of_string "H") in
   fun () ->
-- 
cgit v1.2.3


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

---
 engine/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 83f07d2c62..5581b16562 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -268,7 +268,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
 
 (* Get the last arg of an application *)
 let last_arg sigma c = match EConstr.kind sigma c with
-  | App (f,cl) -> EConstr.Unsafe.to_constr (Array.last cl)
+  | App (f,cl) -> Array.last cl
   | _ -> anomaly (Pp.str "last_arg")
 
 (* Get the last arg of an application *)
-- 
cgit v1.2.3


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

---
 engine/termops.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 5581b16562..59dbb73f54 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -829,6 +829,15 @@ let global_of_constr sigma c =
   | Var id -> VarRef id, Univ.Instance.empty
   | _ -> raise Not_found
 
+let is_global sigma c t =
+  let open Globnames in
+  match c, EConstr.kind sigma t with
+  | ConstRef c, Const (c', _) -> Constant.equal c c'
+  | IndRef i, Ind (i', _) -> eq_ind i i'
+  | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+  | VarRef id, Var id' -> Id.equal id id'
+  | _ -> false
+
 let isGlobalRef sigma c =
   match EConstr.kind sigma c with
   | Const _ | Ind _ | Construct _ | Var _ -> true
-- 
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.

---
 engine/termops.ml | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 59dbb73f54..b7932665a4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -159,6 +159,7 @@ let print_env env =
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
 
 let rel_list n m =
+  let open EConstr in
   let rec reln l p =
     if p>m then l else reln (mkRel(n+p)::l) (p+1)
   in
@@ -857,16 +858,18 @@ let base_sort_cmp pb s0 s1 =
     | _ -> false
 
 (* eq_constr extended with universe erasure *)
-let compare_constr_univ f cv_pb t1 t2 =
-  match kind_of_term t1, kind_of_term t2 with
+let compare_constr_univ sigma f cv_pb t1 t2 =
+  match EConstr.kind sigma t1, EConstr.kind sigma t2 with
       Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	f Reduction.CONV t1 t2 && f cv_pb c1 c2
-    | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
+    | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
 
-let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
+let constr_cmp sigma cv_pb t1 t2 =
+  let rec compare cv_pb t1 t2 = compare_constr_univ sigma compare cv_pb t1 t2 in
+  compare cv_pb t1 t2
 
-let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2
+let eq_constr sigma t1 t2 = constr_cmp sigma Reduction.CONV t1 t2
 
 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
    App(c,[||]) -> ([],c) *)
@@ -883,12 +886,12 @@ type subst = (Context.Rel.t * constr) Evar.Map.t
 
 exception CannotFilter
 
-let filtering env cv_pb c1 c2 =
+let filtering sigma env cv_pb c1 c2 =
   let evm = ref Evar.Map.empty in
   let define cv_pb e1 ev c1 =
     try let (e2,c2) = Evar.Map.find ev !evm in
     let shift = List.length e1 - List.length e2 in
-    if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+    if constr_cmp sigma cv_pb (EConstr.of_constr c1) (EConstr.of_constr (lift shift c2)) then () else raise CannotFilter
     with Not_found ->
       evm := Evar.Map.add ev (e1,c1) !evm
   in
@@ -909,8 +912,9 @@ let filtering env cv_pb c1 c2 =
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
-	  if compare_constr_univ
-	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+          let inj = EConstr.Unsafe.to_constr in
+	  if compare_constr_univ sigma
+	  (fun pb c1 c2 -> aux env pb (inj c1) (inj c2); true) cv_pb (EConstr.of_constr c1) (EConstr.of_constr c2) then ()
 	  else raise CannotFilter
 	  (* TODO: le reste des binders *)
   in
-- 
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.

---
 engine/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index b7932665a4..c2d862f005 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1074,7 +1074,7 @@ let global_vars_set env sigma constr =
   let rec filtrec acc c =
     let acc = match EConstr.kind sigma c with
     | Var _ | Const _ | Ind _ | Construct _ ->
-      Id.Set.union (vars_of_global env (EConstr.Unsafe.to_constr c)) acc
+      Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
     | _ -> acc
     in
     EConstr.fold sigma filtrec acc c
-- 
cgit v1.2.3


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

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

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index c2d862f005..4ab9f0733f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -224,8 +224,8 @@ let mkProd_wo_LetIn decl c =
     | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c)
     | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c
 
-let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
-let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
+let it_mkProd init = List.fold_left (fun c (n,t)  -> EConstr.mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t)  -> EConstr.mkLambda (n, t, c)) init
 
 let it_named_context_quantifier f ~init =
   List.fold_left (fun c d -> f d c) init
-- 
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.

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

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 4ab9f0733f..ef7cdc38b5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -233,9 +233,9 @@ let it_named_context_quantifier f ~init =
 let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
 let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
 let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
-let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier EConstr.mkNamedProd_or_LetIn ~init
 let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
-let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier EConstr.mkNamedLambda_or_LetIn ~init
 
 let it_mkLambda_or_LetIn_from_no_LetIn c decls =
   let open RelDecl in
-- 
cgit v1.2.3


From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 02:45:54 +0100
Subject: Hints API using EConstr.

---
 engine/termops.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index ef7cdc38b5..7c89f190f2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -263,9 +263,10 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
   (* Removed trailing extra implicit arguments, what improves compatibility
      for constants with recently added maximal implicit arguments *)
   | App (f,args) when EConstr.isEvar sigma (Array.last args) ->
+      let open EConstr in
       drop_extra_implicit_args sigma
-	(EConstr.mkApp (f,fst (Array.chop (Array.length args - 1) args)))
-  | _ -> EConstr.Unsafe.to_constr c
+	(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+  | _ -> c
 
 (* Get the last arg of an application *)
 let last_arg sigma c = match EConstr.kind sigma c with
-- 
cgit v1.2.3


From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 03:04:13 +0100
Subject: Rewrite API using EConstr.

---
 engine/termops.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 7c89f190f2..ecc6ab68ea 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -858,6 +858,11 @@ let base_sort_cmp pb s0 s1 =
     | (Type u1, Type u2) -> true
     | _ -> false
 
+let rec is_Prop sigma c = match EConstr.kind sigma c with
+  | Sort (Prop Null) -> true
+  | Cast (c,_,_) -> is_Prop sigma c
+  | _ -> false
+
 (* eq_constr extended with universe erasure *)
 let compare_constr_univ sigma f cv_pb t1 t2 =
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
-- 
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

---
 engine/termops.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index ecc6ab68ea..abaa409bd9 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -276,10 +276,11 @@ let last_arg sigma c = match EConstr.kind sigma c with
 (* Get the last arg of an application *)
 let decompose_app_vect sigma c =
   match EConstr.kind sigma c with
-  | App (f,cl) -> (EConstr.Unsafe.to_constr f, Array.map EConstr.Unsafe.to_constr cl)
-  | _ -> (EConstr.Unsafe.to_constr c,[||])
+  | App (f,cl) -> (f, cl)
+  | _ -> (c,[||])
 
 let adjust_app_list_size f1 l1 f2 l2 =
+  let open EConstr in
   let len1 = List.length l1 and len2 = List.length l2 in
   if Int.equal len1 len2 then (f1,l1,f2,l2)
   else if len1 < len2 then
@@ -698,13 +699,13 @@ let rec subst_meta bl c =
 
 let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
   | Cast (c,_,_) -> strip_outer_cast sigma c
-  | _ -> EConstr.Unsafe.to_constr c
+  | _ -> c
 
 (* flattens application lists throwing casts in-between *)
 let collapse_appl sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
-        match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma f)) with
+        match EConstr.kind sigma (strip_outer_cast sigma f) with
         | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
         | _ -> EConstr.mkApp (f,cl2)
       in
@@ -744,15 +745,17 @@ let my_prefix_application sigma eq_fun (k,c) by_c t =
    works if [c] has rels *)
 
 let subst_term_gen sigma eq_fun c t =
+  let open EConstr in
+  let open Vars in
   let rec substrec (k,c as kc) t =
     match prefix_application sigma eq_fun kc t with
       | Some x -> x
       | None ->
     if eq_fun sigma c t then EConstr.mkRel k
     else
-      EConstr.map_with_binders sigma (fun (k,c) -> (k+1, EConstr.Vars.lift 1 c)) substrec kc t
+      EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
   in
-  EConstr.Unsafe.to_constr (substrec (1,c) t)
+  substrec (1,c) t
 
 let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t
 
-- 
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.

---
 engine/termops.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index abaa409bd9..879d77de2a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -692,6 +692,9 @@ type meta_type_map = (metavariable * types) list
 
 type meta_value_map = (metavariable * constr) list
 
+let isMetaOf sigma mv c =
+  match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false
+
 let rec subst_meta bl c =
   match kind_of_term c with
     | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
-- 
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.

---
 engine/termops.ml | 70 +++++++++++++++++++++++++++----------------------------
 1 file changed, 35 insertions(+), 35 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 879d77de2a..465832c10d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -210,12 +210,7 @@ let lookup_rel_id id sign =
   lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
-let mkProd_or_LetIn decl c =
-  let open RelDecl in
-  match decl with
-    | LocalAssum (na,t) -> mkProd (na, t, c)
-    | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
-
+let mkProd_or_LetIn = EConstr.mkProd_or_LetIn
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
 let mkProd_wo_LetIn decl c =
   let open EConstr in
@@ -628,9 +623,10 @@ let vars_of_global_reference env gr =
    [m] is appropriately lifted through abstractions of [t] *)
 
 let dependent_main noevar univs sigma m t =
+  let open EConstr in
   let eqc x y =
-    if univs then not (Option.is_empty (EConstr.eq_constr_universes sigma x y))
-    else EConstr.eq_constr_nounivs sigma x y
+    if univs then not (Option.is_empty (eq_constr_universes sigma x y))
+    else eq_constr_nounivs sigma x y
   in
   let rec deprec m t =
     if eqc m t then
@@ -638,13 +634,13 @@ let dependent_main noevar univs sigma m t =
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    deprec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
 	    CArray.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when noevar && EConstr.isMeta sigma c -> ()
+	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
 	| _, Evar _ when noevar -> ()
-	| _ -> EConstr.iter_with_binders sigma (fun c -> EConstr.Vars.lift 1 c) deprec m t
+	| _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
   in
   try deprec m t; false with Occur -> true
 
@@ -661,6 +657,7 @@ let dependent_in_decl sigma a decl =
     | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t)
 
 let count_occurrences sigma m t =
+  let open EConstr in
   let n = ref 0 in
   let rec countrec m t =
     if EConstr.eq_constr sigma m t then
@@ -668,13 +665,13 @@ let count_occurrences sigma m t =
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    countrec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
 	    Array.iter (countrec m)
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when EConstr.isMeta sigma c -> ()
+	| _, Cast (c,_,_) when isMeta sigma c -> ()
 	| _, Evar _ -> ()
-	| _ -> EConstr.iter_with_binders sigma (EConstr.Vars.lift 1) countrec m t
+	| _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
   in
   countrec m t;
   !n
@@ -682,7 +679,7 @@ let count_occurrences sigma m t =
 (* Synonymous *)
 let occur_term = dependent
 
-let pop t = EConstr.Unsafe.to_constr (EConstr.Vars.lift (-1) t)
+let pop t = EConstr.Vars.lift (-1) t
 
 (***************************)
 (*  bindings functions *)
@@ -712,33 +709,35 @@ let collapse_appl sigma c = match EConstr.kind sigma c with
         | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
         | _ -> EConstr.mkApp (f,cl2)
       in
-      EConstr.Unsafe.to_constr (collapse_rec f cl)
-  | _ -> EConstr.Unsafe.to_constr c
+      collapse_rec f cl
+  | _ -> c
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
 let prefix_application sigma eq_fun (k,c) t =
-  let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in
+  let open EConstr in
+  let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (EConstr.mkApp (EConstr.mkRel k, Array.sub cl2 l1 (l2 - l1)))
+	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else
 	  None
     | _ -> None
 
 let my_prefix_application sigma eq_fun (k,c) by_c t =
-  let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in
+  let open EConstr in
+  let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (EConstr.mkApp ((EConstr.Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
 	else
 	  None
     | _ -> None
@@ -754,7 +753,7 @@ let subst_term_gen sigma eq_fun c t =
     match prefix_application sigma eq_fun kc t with
       | Some x -> x
       | None ->
-    if eq_fun sigma c t then EConstr.mkRel k
+    if eq_fun sigma c t then mkRel k
     else
       EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
   in
@@ -775,7 +774,7 @@ let replace_term_gen sigma eq_fun c by_c in_t =
       EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
 	substrec kc t)
   in
-  EConstr.Unsafe.to_constr (substrec (0,c) in_t)
+  substrec (0,c) in_t
 
 let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t
 
@@ -933,12 +932,11 @@ let filtering sigma env cv_pb c1 c2 =
   aux env cv_pb c1 c2; !evm
 
 let decompose_prod_letin sigma c =
-  let inj c = EConstr.Unsafe.to_constr c in
   let rec prodec_rec i l sigma c = match EConstr.kind sigma c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n, inj t)::l) sigma c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n, inj d, inj t)::l) sigma c
+    | Prod (n,t,c)    -> prodec_rec (succ i) (local_assum (n, t)::l) sigma c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (local_def (n, d, t)::l) sigma c
     | Cast (c,_,_)    -> prodec_rec i l sigma c
-    | _               -> i,l, inj c in
+    | _               -> i,l, c in
   prodec_rec 0 [] sigma c
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
@@ -969,7 +967,7 @@ let nb_prod_modulo_zeta sigma x =
       | _ -> n
   in count 0 x
 
-let align_prod_letin sigma c a : Context.Rel.t * constr =
+let align_prod_letin sigma c a =
   let (lc,_,_) = decompose_prod_letin sigma c in
   let (la,l,a) = decompose_prod_letin sigma a in
   if not (la >= lc) then invalid_arg "align_prod_letin";
@@ -980,21 +978,23 @@ let align_prod_letin sigma c a : Context.Rel.t * constr =
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 earlier buggish versions                      *)
 
-let rec eta_reduce_head c =
-  match kind_of_term c with
+let rec eta_reduce_head sigma c =
+  let open EConstr in
+  let open Vars in
+  match EConstr.kind sigma c with
     | Lambda (_,c1,c') ->
-	(match kind_of_term (eta_reduce_head c') with
+	(match EConstr.kind sigma (eta_reduce_head sigma c') with
            | App (f,cl) ->
                let lastn = (Array.length cl) - 1 in
                if lastn < 0 then anomaly (Pp.str "application without arguments")
                else
-                 (match kind_of_term cl.(lastn) with
+                 (match EConstr.kind sigma cl.(lastn) with
                     | Rel 1 ->
 			let c' =
                           if Int.equal lastn 0 then f
 			  else mkApp (f, Array.sub cl 0 lastn)
 			in
-			if noccurn 1 c'
+			if noccurn sigma 1 c'
                         then lift (-1) c'
                         else c
                     | _   -> c)
-- 
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.

---
 engine/termops.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 465832c10d..46e9ad927f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -97,11 +97,11 @@ let rec pr_constr c = match kind_of_term c with
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref (fun _ -> pr_constr)
-let print_constr_env t = !term_printer t
-let print_constr t = !term_printer (Global.env()) t
+let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let print_constr_env env sigma t = !term_printer env sigma t
+let print_constr t = !term_printer (Global.env()) Evd.empty t
 let set_print_constr f = term_printer := f
-let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c)
+let () = Hook.set Evd.print_constr_hook (fun env sigma c -> !term_printer env sigma (EConstr.of_constr c))
 
 let pr_var_decl env decl =
   let open NamedDecl in
@@ -109,9 +109,10 @@ let pr_var_decl env decl =
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
-	let pb = print_constr_env env c in
+	let c = EConstr.of_constr c in
+	let pb = print_constr_env env Evd.empty c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env (get_type decl) in
+  let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
@@ -121,9 +122,10 @@ let pr_rel_decl env decl =
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
-	let pb = print_constr_env env c in
+	let c = EConstr.of_constr c in
+	let pb = print_constr_env env Evd.empty c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env (get_type decl) in
+  let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
-- 
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.
---
 engine/termops.ml | 94 ++++++++++++++++++++++++++++---------------------------
 1 file changed, 48 insertions(+), 46 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 46e9ad927f..c35e92f97c 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -167,19 +167,10 @@ let rel_list n m =
   in
   reln [] 1
 
-let local_assum (na, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let push_rel_assum (x,t) env =
   let open RelDecl in
-  push_rel (local_assum (x,t)) env
+  let open EConstr in
+  push_rel (LocalAssum (x,t)) env
 
 let push_rels_assum assums =
   let open RelDecl in
@@ -218,8 +209,8 @@ let mkProd_wo_LetIn decl c =
   let open EConstr in
   let open RelDecl in
   match decl with
-    | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c)
-    | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (_,b,_) -> Vars.subst1 b c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> EConstr.mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> EConstr.mkLambda (n, t, c)) init
@@ -334,7 +325,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
 
 let fold_rec_types g (lna,typarray,_) e =
   let open EConstr in
-  let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in
+  let open Vars in
+  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -350,6 +342,7 @@ let map_left2 f a g b =
   end
 
 let map_constr_with_binders_left_to_right sigma g f l c =
+  let open RelDecl in
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -361,18 +354,18 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (local_assum (na,t)) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (local_assum (na,t)) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (local_def (na,bo,t)) l) b in
+      let b' = f (g (LocalDef (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
@@ -414,7 +407,6 @@ let map_constr_with_binders_left_to_right sigma g f l c =
 
 (* strong *)
 let map_constr_with_full_binders sigma g f l cstr =
-  let inj c = EConstr.Unsafe.to_constr c in
   let open EConstr in
   let open RelDecl in
   match EConstr.kind sigma cstr with
@@ -426,16 +418,16 @@ let map_constr_with_full_binders sigma g f l cstr =
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na, inj t)) l) c in
+      let c' = f (g (LocalAssum (na, t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na, inj t)) l) c in
+      let c' = f (g (LocalAssum (na, t)) l) c in
       if t==t' && c==c' then cstr else  mkLambda (na, t', c')
   | LetIn (na,b,t,c) ->
       let b' = f l b in
       let t' = f l t in
-      let c' = f (g (LocalDef (na, inj b, inj t)) l) c in
+      let c' = f (g (LocalDef (na, b, t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -456,7 +448,7 @@ let map_constr_with_full_binders sigma g f l cstr =
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -464,7 +456,7 @@ let map_constr_with_full_binders sigma g f l cstr =
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -577,10 +569,10 @@ let occur_var env sigma id c =
 let occur_var_in_decl env sigma hyp decl =
   let open NamedDecl in
   match decl with
-    | LocalAssum (_,typ) -> occur_var env sigma hyp (EConstr.of_constr typ)
+    | LocalAssum (_,typ) -> occur_var env sigma hyp typ
     | LocalDef (_, body, typ) ->
-        occur_var env sigma hyp (EConstr.of_constr typ) ||
-        occur_var env sigma hyp (EConstr.of_constr body)
+        occur_var env sigma hyp typ ||
+        occur_var env sigma hyp body
 
 let local_occur_var sigma id c =
   let rec occur c = match EConstr.kind sigma c with
@@ -655,8 +647,8 @@ let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t
 let dependent_in_decl sigma a decl =
   let open NamedDecl in
   match decl with
-    | LocalAssum (_,t) -> dependent sigma a (EConstr.of_constr t)
-    | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t)
+    | LocalAssum (_,t) -> dependent sigma a t
+    | LocalDef (_, body, t) -> dependent sigma a body || dependent sigma a t
 
 let count_occurrences sigma m t =
   let open EConstr in
@@ -886,7 +878,7 @@ let eq_constr sigma t1 t2 = constr_cmp sigma Reduction.CONV t1 t2
 
 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
    App(c,[||]) -> ([],c) *)
-let split_app c = match kind_of_term c with
+let split_app sigma c = match EConstr.kind sigma c with
     App(c,l) ->
       let len = Array.length l in
       if Int.equal len 0 then ([],c) else
@@ -895,28 +887,30 @@ let split_app c = match kind_of_term c with
 	c::(Array.to_list prev), last
   | _ -> assert false
 
-type subst = (Context.Rel.t * constr) Evar.Map.t
+type subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t
 
 exception CannotFilter
 
 let filtering sigma env cv_pb c1 c2 =
+  let open EConstr in
+  let open Vars in
   let evm = ref Evar.Map.empty in
   let define cv_pb e1 ev c1 =
     try let (e2,c2) = Evar.Map.find ev !evm in
     let shift = List.length e1 - List.length e2 in
-    if constr_cmp sigma cv_pb (EConstr.of_constr c1) (EConstr.of_constr (lift shift c2)) then () else raise CannotFilter
+    if constr_cmp sigma cv_pb c1 (lift shift c2) then () else raise CannotFilter
     with Not_found ->
       evm := Evar.Map.add ev (e1,c1) !evm
   in
   let rec aux env cv_pb c1 c2 =
-    match kind_of_term c1, kind_of_term c2 with
+    match EConstr.kind sigma c1, EConstr.kind sigma c2 with
       | App _, App _ ->
-        let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+        let ((p1,l1),(p2,l2)) = (split_app sigma c1),(split_app sigma c2) in
         let () = aux env cv_pb l1 l2 in
         begin match p1, p2 with
         | [], [] -> ()
         | (h1 :: p1), (h2 :: p2) ->
-          aux env cv_pb (applistc h1 p1) (applistc h2 p2)
+          aux env cv_pb (applist (h1, p1)) (applist (h2, p2))
         | _ -> assert false
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
@@ -925,21 +919,20 @@ let filtering sigma env cv_pb c1 c2 =
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
-          let inj = EConstr.Unsafe.to_constr in
 	  if compare_constr_univ sigma
-	  (fun pb c1 c2 -> aux env pb (inj c1) (inj c2); true) cv_pb (EConstr.of_constr c1) (EConstr.of_constr c2) then ()
+	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
 	  else raise CannotFilter
 	  (* TODO: le reste des binders *)
   in
   aux env cv_pb c1 c2; !evm
 
 let decompose_prod_letin sigma c =
-  let rec prodec_rec i l sigma c = match EConstr.kind sigma c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) (local_assum (n, t)::l) sigma c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) (local_def (n, d, t)::l) sigma c
-    | Cast (c,_,_)    -> prodec_rec i l sigma c
-    | _               -> i,l, c in
-  prodec_rec 0 [] sigma c
+  let rec prodec_rec i l c = match EConstr.kind sigma c with
+    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
+    | Cast (c,_,_)    -> prodec_rec i l c
+    | _               -> i,l,c in
+  prodec_rec 0 [] c
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
@@ -1007,7 +1000,7 @@ let rec eta_reduce_head sigma c =
 (* iterator on rel context *)
 let process_rel_context f env =
   let sign = named_context_val env in
-  let rels = rel_context env in
+  let rels = EConstr.rel_context env in
   let env0 = reset_with_named_context sign env in
   Context.Rel.fold_outside f rels ~init:env0
 
@@ -1055,6 +1048,14 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 let mem_named_context_val id ctxt =
   try Environ.lookup_named_val id ctxt; true with Not_found -> false
 
+let map_rel_decl f = function
+| RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)
+| RelDecl.LocalDef (id, b, t) -> RelDecl.LocalDef (id, f b, f t)
+
+let map_named_decl f = function
+| NamedDecl.LocalAssum (id, t) -> NamedDecl.LocalAssum (id, f t)
+| NamedDecl.LocalDef (id, b, t) -> NamedDecl.LocalDef (id, f b, f t)
+
 let compact_named_context sign =
   let compact l decl =
     match decl, l with
@@ -1098,10 +1099,10 @@ let global_vars_set env sigma constr =
 let global_vars env sigma ids = Id.Set.elements (global_vars_set env sigma ids)
 
 let global_vars_set_of_decl env sigma = function
-  | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma (EConstr.of_constr t)
+  | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma t
   | NamedDecl.LocalDef (_,c,t) ->
-      Id.Set.union (global_vars_set env sigma (EConstr.of_constr t))
-        (global_vars_set env sigma (EConstr.of_constr c))
+      Id.Set.union (global_vars_set env sigma t)
+        (global_vars_set env sigma c)
 
 let dependency_closure env sigma sign hyps =
   if Id.Set.is_empty hyps then [] else
@@ -1155,6 +1156,7 @@ let context_chop k ctx =
 
 (* Do not skip let-in's *)
 let env_rel_context_chop k env =
+  let open EConstr in
   let rels = rel_context env in
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
-- 
cgit v1.2.3


From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 23:48:28 +0100
Subject: Moving printing code from Evd to Termops.

---
 engine/termops.ml | 324 +++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 323 insertions(+), 1 deletion(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index c35e92f97c..ff1a0d9de9 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -101,7 +101,329 @@ let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr
 let print_constr_env env sigma t = !term_printer env sigma t
 let print_constr t = !term_printer (Global.env()) Evd.empty t
 let set_print_constr f = term_printer := f
-let () = Hook.set Evd.print_constr_hook (fun env sigma c -> !term_printer env sigma (EConstr.of_constr c))
+
+module EvMap = Evar.Map
+
+let pr_evar_suggested_name evk sigma =
+  let open Evd in
+  let base_id evk' evi =
+  match evar_ident evk' sigma with
+  | Some id -> id
+  | None -> match evi.evar_source with
+  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+  | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+  | _ ->
+      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+  in
+  let names = EvMap.mapi base_id (undefined_map sigma) in
+  let id = EvMap.find evk names in
+  let fold evk' id' (seen, n) =
+    if seen then (seen, n)
+    else if Evar.equal evk evk' then (true, n)
+    else if Id.equal id id' then (seen, succ n)
+    else (seen, n)
+  in
+  let (_, n) = EvMap.fold fold names (false, 0) in
+  if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk =
+let open Evd in
+match evar_ident evk sigma with
+| None ->
+  str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+  str "?" ++ pr_id id
+
+let pr_instance_status (sc,typ) =
+  let open Evd in
+  begin match sc with
+  | IsSubType -> str " [or a subtype of it]"
+  | IsSuperType -> str " [or a supertype of it]"
+  | Conv -> mt ()
+  end ++
+  begin match typ with
+  | CoerceToType -> str " [up to coercion]"
+  | TypeNotProcessed -> mt ()
+  | TypeProcessed -> str " [type is checked]"
+  end
+
+let protect f x =
+  try f x
+  with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+
+let print_kconstr a =
+  protect (fun c -> print_constr (EConstr.of_constr c)) a
+
+let pr_meta_map evd =
+  let open Evd in
+  let print_constr = print_kconstr in
+  let pr_name = function
+      Name id -> str"[" ++ pr_id id ++ str"]"
+    | _ -> mt() in
+  let pr_meta_binding = function
+    | (mv,Cltyp (na,b)) ->
+      	hov 0
+	  (pr_meta mv ++ pr_name na ++ str " : " ++
+           print_constr b.rebus ++ fnl ())
+    | (mv,Clval(na,(b,s),t)) ->
+      	hov 0
+	  (pr_meta mv ++ pr_name na ++ str " := " ++
+           print_constr b.rebus ++
+	   str " : " ++ print_constr t.rebus ++
+	   spc () ++ pr_instance_status s ++ fnl ())
+  in
+  prlist pr_meta_binding (meta_list evd)
+
+let pr_decl (decl,ok) =
+  let open NamedDecl in
+  let print_constr = print_kconstr in
+  match decl with
+  | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+  | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
+                           print_constr c ++ str (if ok then ")" else "}")
+
+let pr_evar_source = function
+  | Evar_kinds.QuestionMark _ -> str "underscore"
+  | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
+  | Evar_kinds.CasesType true ->
+      str "subterm of pattern-matching return predicate"
+  | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
+  | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+  | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
+      let open Globnames in
+      let print_constr = print_kconstr in
+      let id = Option.get ido in
+      str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
+      spc () ++ print_constr (printable_constr_of_global c)
+  | Evar_kinds.InternalHole -> str "internal placeholder"
+  | Evar_kinds.TomatchTypeParameter (ind,n) ->
+      let print_constr = print_kconstr in
+      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+  | Evar_kinds.GoalEvar -> str "goal evar"
+  | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
+  | Evar_kinds.MatchingVar _ -> str "matching variable"
+  | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
+  | Evar_kinds.SubEvar evk ->
+      let open Evd in
+      str "subterm of " ++ str (string_of_existential evk)
+
+let pr_evar_info evi =
+  let open Evd in
+  let print_constr = print_kconstr in
+  let phyps =
+    try
+      let decls = match Filter.repr (evar_filter evi) with
+      | None -> List.map (fun c -> (c, true)) (evar_context evi)
+      | Some filter -> List.combine (evar_context evi) filter
+      in
+      prlist_with_sep spc pr_decl (List.rev decls)
+    with Invalid_argument _ -> str "Ill-formed filtered context" in
+  let pty = print_constr evi.evar_concl in
+  let pb =
+    match evi.evar_body with
+      | Evar_empty -> mt ()
+      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+  in
+  let candidates =
+    match evi.evar_body, evi.evar_candidates with
+      | Evar_empty, Some l ->
+           spc () ++ str "{" ++
+           prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+      | _ ->
+          mt ()
+  in
+  let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
+  hov 2
+    (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]" ++
+       candidates ++ spc() ++ src)
+
+let compute_evar_dependency_graph sigma =
+  let open Evd in
+  (* Compute the map binding ev to the evars whose body depends on ev *)
+  let fold evk evi acc =
+    let fold_ev evk' acc =
+      let tab =
+        try EvMap.find evk' acc
+        with Not_found -> Evar.Set.empty
+      in
+      EvMap.add evk' (Evar.Set.add evk tab) acc
+    in
+    match evar_body evi with
+    | Evar_empty -> acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+  in
+  Evd.fold fold sigma EvMap.empty
+
+let evar_dependency_closure n sigma =
+  let open Evd in
+  (** Create the DAG of depth [n] representing the recursive dependencies of
+      undefined evars. *)
+  let graph = compute_evar_dependency_graph sigma in
+  let rec aux n curr accu =
+    if Int.equal n 0 then Evar.Set.union curr accu
+    else
+      let fold evk accu =
+        try
+          let deps = EvMap.find evk graph in
+          Evar.Set.union deps accu
+        with Not_found -> accu
+      in
+      (** Consider only the newly added evars *)
+      let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
+      (** Merge the others *)
+      let accu = Evar.Set.union curr accu in
+      aux (n - 1) ncurr accu
+  in
+  let undef = EvMap.domain (undefined_map sigma) in
+  aux n undef Evar.Set.empty
+
+let evar_dependency_closure n sigma =
+  let open Evd in
+  let deps = evar_dependency_closure n sigma in
+  let map = EvMap.bind (fun ev -> find sigma ev) deps in
+  EvMap.bindings map
+
+let has_no_evar sigma =
+  try let () = Evd.fold (fun _ _ () -> raise Exit) sigma () in true
+  with Exit -> false
+
+let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+
+let pr_evar_universe_context ctx =
+  let open UState in
+  let open Evd in
+  let prl = pr_uctx_level ctx in
+  if UState.is_empty ctx then mt ()
+  else
+    (str"UNIVERSES:"++brk(0,1)++ 
+       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
+     str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
+     h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
+     str"UNDEFINED UNIVERSES:"++brk(0,1)++
+       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
+
+let print_env_short env =
+  let print_constr = print_kconstr in
+  let pr_rel_decl = function
+    | RelDecl.LocalAssum (n,_) -> pr_name n
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+  in
+  let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
+  let nc = List.rev (named_context env) in
+  let rc = List.rev (rel_context env) in
+    str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
+    str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
+
+let pr_evar_constraints pbs =
+  let pr_evconstr (pbty, env, t1, t2) =
+    let env =
+      (** We currently allow evar instances to refer to anonymous de
+          Bruijn indices, so we protect the error printing code in this
+          case by giving names to every de Bruijn variable in the
+          rel_context of the conversion problem. MS: we should rather
+          stop depending on anonymous variables, they can be used to
+          indicate independency. Also, this depends on a strategy for
+          naming/renaming. *)
+      Namegen.make_all_name_different env
+    in
+    print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+      print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++
+      str (match pbty with
+            | Reduction.CONV -> "=="
+            | Reduction.CUMUL -> "<=") ++
+      spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+  in
+  prlist_with_sep fnl pr_evconstr pbs
+
+let pr_evar_map_gen with_univs pr_evars sigma =
+  let uvs = Evd.evar_universe_context sigma in
+  let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in
+  let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
+  and svs = if with_univs then pr_evar_universe_context uvs else mt ()
+  and cstrs =
+    if List.is_empty conv_pbs then mt ()
+    else
+    str "CONSTRAINTS:" ++ brk (0, 1) ++
+      pr_evar_constraints conv_pbs ++ fnl ()
+  and metas =
+    if List.is_empty (Evd.meta_list sigma) then mt ()
+    else
+      str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
+  in
+  evs ++ svs ++ cstrs ++ metas
+
+let pr_evar_list sigma l =
+  let open Evd in
+  let pr (ev, evi) =
+    h 0 (str (string_of_existential ev) ++
+      str "==" ++ pr_evar_info evi ++
+      (if evi.evar_body == Evar_empty
+       then str " {" ++  pr_existential_key sigma ev ++ str "}"
+       else mt ()))
+  in
+  h 0 (prlist_with_sep fnl pr l)
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
+  (* Print all evars *)
+  let to_list d =
+    let open Evd in
+    (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
+    let l = ref [] in
+    let fold_def evk evi () = match evi.evar_body with
+    | Evar_defined _ -> l := (evk, evi) :: !l
+    | Evar_empty -> ()
+    in
+    let fold_undef evk evi () = match evi.evar_body with
+    | Evar_empty -> l := (evk, evi) :: !l
+    | Evar_defined _ -> ()
+    in
+    Evd.fold fold_def d ();
+    Evd.fold fold_undef d ();
+    !l
+  in
+  str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
+| Some n ->
+  (* Print all evars *)
+  str"UNDEFINED EVARS:"++
+  (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
+  brk(0,1)++
+  pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
+
+let pr_evar_by_filter filter sigma =
+  let open Evd in
+  let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in
+  let elts = List.rev elts in
+  let is_def (_, evi) = match evi.evar_body with
+  | Evar_defined _ -> true
+  | Evar_empty -> false
+  in
+  let (defined, undefined) = List.partition is_def elts in
+  let filter (evk, evi) = filter evk evi in
+  let defined = List.filter filter defined in
+  let undefined = List.filter filter undefined in
+  let prdef =
+    if List.is_empty defined then mt ()
+    else str "DEFINED EVARS:" ++ brk (0, 1) ++
+      pr_evar_list sigma defined
+  in
+  let prundef =
+    if List.is_empty undefined then mt ()
+    else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
+      pr_evar_list sigma undefined
+  in
+  prdef ++ prundef
+
+let pr_evar_map ?(with_univs=true) depth sigma =
+  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
+
+let pr_evar_map_filter ?(with_univs=true) filter sigma =
+  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
+
+let pr_metaset metas =
+  str "[" ++ pr_sequence pr_meta (Evd.Metaset.elements metas) ++ str "]"
 
 let pr_var_decl env decl =
   let open NamedDecl in
-- 
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.
---
 engine/termops.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index ff1a0d9de9..d8e712abc7 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma =
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+      Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
   in
   let names = EvMap.mapi base_id (undefined_map sigma) in
   let id = EvMap.find evk names in
@@ -316,7 +316,7 @@ let print_env_short env =
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
     str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
 
-let pr_evar_constraints pbs =
+let pr_evar_constraints sigma pbs =
   let pr_evconstr (pbty, env, t1, t2) =
     let env =
       (** We currently allow evar instances to refer to anonymous de
@@ -326,10 +326,10 @@ let pr_evar_constraints pbs =
           stop depending on anonymous variables, they can be used to
           indicate independency. Also, this depends on a strategy for
           naming/renaming. *)
-      Namegen.make_all_name_different env
+      Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++
+      print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
@@ -346,7 +346,7 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     if List.is_empty conv_pbs then mt ()
     else
     str "CONSTRAINTS:" ++ brk (0, 1) ++
-      pr_evar_constraints conv_pbs ++ fnl ()
+      pr_evar_constraints sigma conv_pbs ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
-- 
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.
---
 engine/termops.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 410fb75c5f..a679163456 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1181,14 +1181,19 @@ let base_sort_cmp pb s0 s1 =
     | _ -> false
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
-  | Sort (Prop Null) -> true
+  | Sort u ->
+    begin match EConstr.ESorts.kind sigma u with
+    | Prop Null -> true
+    | _ -> false
+    end
   | Cast (c,_,_) -> is_Prop sigma c
   | _ -> false
 
 (* eq_constr extended with universe erasure *)
 let compare_constr_univ sigma f cv_pb t1 t2 =
+  let open EConstr in
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
-      Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+      Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	f Reduction.CONV t1 t2 && f cv_pb c1 c2
     | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
-- 
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.
---
 engine/termops.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index a679163456..64f4c6dc5e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1150,7 +1150,7 @@ let global_of_constr sigma c =
   | Const (c, u) -> ConstRef c, u
   | Ind (i, u) -> IndRef i, u
   | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Univ.Instance.empty
+  | Var id -> VarRef id, EConstr.EInstance.empty
   | _ -> raise Not_found
 
 let is_global sigma c t =
@@ -1169,8 +1169,12 @@ let isGlobalRef sigma c =
 
 let is_template_polymorphic env sigma f =
   match EConstr.kind sigma f with
-  | Ind ind -> Environ.template_polymorphic_pind ind env
-  | Const c -> Environ.template_polymorphic_pconstant c env
+  | Ind (ind, u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_ind ind env
+  | Const (cst, u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_constant cst env
   | _ -> false
 
 let base_sort_cmp pb s0 s1 =
@@ -1453,8 +1457,8 @@ let global_app_of_constr sigma c =
   | Const (c, u) -> (ConstRef c, u), None
   | Ind (i, u) -> (IndRef i, u), None
   | Construct (c, u) -> (ConstructRef c, u), None
-  | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
+  | Var id -> (VarRef id, EConstr.EInstance.empty), None
+  | Proj (p, c) -> (ConstRef (Projection.constant p), EConstr.EInstance.empty), Some c
   | _ -> raise Not_found
 
 let prod_applist sigma c l =
-- 
cgit v1.2.3