Termops API using EConstr.

3 files changed, 209 insertions, 192 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 13444cb379..05f98a41fd 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -540,12 +540,12 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                   (* Check if some id to clear occurs in the instance
                      a of rid in ev and remember the dependency *)
                     let check id = if Id.Set.mem id ids then raise (Depends id) in
-                    let () = Id.Set.iter check (collect_vars a) in
+                    let () = Id.Set.iter check (collect_vars !evdref (EConstr.of_constr a)) in
                   (* Check if some rid to clear in the context of ev
                      has dependencies in another hyp of the context of ev
                      and transitively remember the dependency *)
                     let check id _ =
-                      if occur_var_in_decl (Global.env ()) id h
+                      if occur_var_in_decl (Global.env ()) !evdref id h
                       then raise (Depends id)
                     in
                     let () = Id.Map.iter check ri in
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,[])
diff --git a/engine/termops.mli b/engine/termops.mli
index 78826f79ae..5d53ce09e8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -69,8 +69,9 @@ val map_constr_with_binders_left_to_right :
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
+  Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
-  ('a -> constr -> constr) -> 'a -> constr -> constr
+  ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
@@ -80,11 +81,12 @@ val map_constr_with_full_binders :
    each binder traversal; it is not recursive *)
 
 val fold_constr_with_binders :
-  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
+  Evd.evar_map -> ('a -> 'a) ->
+    ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b
 
 val fold_constr_with_full_binders :
-  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
-    'a -> 'b -> constr -> 'b
+  Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) ->
+    ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b
 
 val iter_constr_with_full_binders :
   (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
@@ -92,39 +94,39 @@ val iter_constr_with_full_binders :
 
 (**********************************************************************)
 
-val strip_head_cast : constr -> constr
-val drop_extra_implicit_args : constr -> constr
+val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t
+val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> constr
 
 (** occur checks *)
 
 exception Occur
-val occur_meta : types -> bool
-val occur_existential : types -> bool
-val occur_meta_or_existential : types -> bool
-val occur_evar : existential_key -> types -> bool
-val occur_var : env -> Id.t -> types -> bool
+val occur_meta : Evd.evar_map -> EConstr.t -> bool
+val occur_existential : Evd.evar_map -> EConstr.t -> bool
+val occur_meta_or_existential : Evd.evar_map -> EConstr.t -> bool
+val occur_evar : Evd.evar_map -> existential_key -> EConstr.t -> bool
+val occur_var : env -> Evd.evar_map -> Id.t -> EConstr.t -> bool
 val occur_var_in_decl :
-  env ->
+  env -> Evd.evar_map ->
   Id.t -> Context.Named.Declaration.t -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
-val local_occur_var : Id.t -> types -> bool
+val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool
 
-val free_rels : constr -> Int.Set.t
+val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t
 
 (** [dependent m t] tests whether [m] is a subterm of [t] *)
-val dependent : constr -> constr -> bool
-val dependent_no_evar : constr -> constr -> bool
-val dependent_univs : constr -> constr -> bool
-val dependent_univs_no_evar : constr -> constr -> bool
-val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
-val count_occurrences : constr -> constr -> int
-val collect_metas : constr -> int list
-val collect_vars : constr -> Id.Set.t (** for visible vars only *)
+val dependent : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
+val dependent_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
+val dependent_univs : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
+val dependent_univs_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
+val dependent_in_decl : Evd.evar_map -> EConstr.t -> Context.Named.Declaration.t -> bool
+val count_occurrences : Evd.evar_map -> EConstr.t -> EConstr.t -> int
+val collect_metas : Evd.evar_map -> EConstr.t -> int list
+val collect_vars : Evd.evar_map -> EConstr.t -> Id.Set.t (** for visible vars only *)
 val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
-val occur_term : constr -> constr -> bool (** Synonymous
- of dependent 
-   Substitution of metavariables *)
+val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *)
+
+(* Substitution of metavariables *)
 type meta_value_map = (metavariable * constr) list
 val subst_meta : meta_value_map -> constr -> constr
 
@@ -132,7 +134,7 @@ val subst_meta : meta_value_map -> constr -> constr
 type meta_type_map = (metavariable * types) list
 
 (** [pop c] lifts by -1 the positive indexes in [c] *)
-val pop : constr -> constr
+val pop : EConstr.t -> constr
 
 (** {6 ... } *)
 (** Substitution of an arbitrary large term. Uses equality modulo
@@ -140,20 +142,20 @@ val pop : constr -> constr
 
 (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
    as equality *)
-val subst_term_gen :
-  (constr -> constr -> bool) -> constr -> constr -> constr
+val subst_term_gen : Evd.evar_map ->
+  (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> constr
 
 (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
    as equality *)
 val replace_term_gen :
-  (constr -> constr -> bool) ->
-    constr -> constr -> constr -> constr
+  Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) ->
+    EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-val subst_term : constr -> constr -> constr
+val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr
 
 (** [replace_term d e c] replaces [d] by [e] in [c] *)
-val replace_term : constr -> constr -> constr -> constr
+val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** Alternative term equalities *)
 val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
@@ -165,11 +167,11 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
 val eta_reduce_head : constr -> constr
 
 (** Flattens application lists *)
-val collapse_appl : constr -> constr
+val collapse_appl : Evd.evar_map -> EConstr.t -> constr
 
 (** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : constr -> constr
+val strip_outer_cast : Evd.evar_map -> EConstr.t -> constr
 
 exception CannotFilter
 
@@ -182,24 +184,24 @@ exception CannotFilter
 type subst = (Context.Rel.t * constr) Evar.Map.t
 val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
 
-val decompose_prod_letin : constr -> int * Context.Rel.t * constr
-val align_prod_letin : constr -> constr -> Context.Rel.t * constr
+val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr
+val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr
 
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
-val nb_lam : constr -> int
+val nb_lam : Evd.evar_map -> EConstr.t -> int
 
 (** Similar to [nb_lam], but gives the number of products instead *)
-val nb_prod : constr -> int
+val nb_prod : Evd.evar_map -> EConstr.t -> int
 
 (** Similar to [nb_prod], but zeta-contracts let-in on the way *)
-val nb_prod_modulo_zeta : constr -> int
+val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int
 
 (** Get the last arg of a constr intended to be an application *)
-val last_arg : constr -> constr
+val last_arg : Evd.evar_map -> EConstr.t -> constr
 
 (** Force the decomposition of a term as an applicative one *)
-val decompose_app_vect : constr -> constr * constr array
+val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array
 
 val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
   (constr * constr list * constr * constr list)
@@ -250,19 +252,19 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t
 
 val clear_named_body : Id.t -> env -> env
 
-val global_vars : env -> constr -> Id.t list
-val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t
+val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
+val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val isGlobalRef : constr -> bool
+val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
 
-val is_template_polymorphic : env -> constr -> bool
+val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
 
 (** Combinators on judgments *)