7 files changed, 816 insertions, 0 deletions

diff --git a/dev/db b/dev/db
index d3503ef43..432baf8a6 100644
--- a/dev/db
+++ b/dev/db
@@ -28,6 +28,7 @@ install_printer Top_printers.pppattern
 install_printer Top_printers.ppglob_constr
 
 install_printer Top_printers.ppconstr
+install_printer Top_printers.ppeconstr
 install_printer Top_printers.ppuni
 install_printer Top_printers.ppuniverses
 install_printer Top_printers.ppconstraints
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b552d9994..b7736f498 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -71,6 +71,7 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 let rawdebug = ref false
 let ppevar evk = pp (str (Evd.string_of_existential evk))
 let ppconstr x = pp (Termops.print_constr x)
+let ppeconstr x = pp (Termops.print_constr (EConstr.Unsafe.to_constr x))
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
 let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
new file mode 100644
index 000000000..0a5f1ba68
--- /dev/null
+++ b/engine/eConstr.ml
@@ -0,0 +1,614 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CSig
+open CErrors
+open Util
+open Names
+open Term
+open Context
+open Evd
+
+module API :
+sig
+type t
+val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
+val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val of_kind : (t, t) Constr.kind_of_term -> t
+val of_constr : Constr.t -> t
+val unsafe_to_constr : t -> Constr.t
+val unsafe_eq : (t, Constr.t) eq
+end =
+struct
+
+type t = Constr.t
+
+let safe_evar_value sigma ev =
+  try Some (Evd.existential_value sigma ev)
+  with NotInstantiatedEvar | Not_found -> None
+
+let rec kind sigma c =
+  let c0 = Constr.kind c in
+  match c0 with
+  | Evar (evk, args) ->
+    (match safe_evar_value sigma (evk, args) with
+        Some c -> kind sigma c
+      | None -> c0)
+  | Sort (Type u) ->
+    let u' = Evd.normalize_universe sigma u in
+    if u' == u then c0 else Sort (Type u')
+  | Const (c', u) when not (Univ.Instance.is_empty u) ->
+    let u' = Evd.normalize_universe_instance sigma u in
+    if u' == u then c0 else Const (c', u')
+  | Ind (i, u) when not (Univ.Instance.is_empty u) ->
+    let u' = Evd.normalize_universe_instance sigma u in
+    if u' == u then c0 else Ind (i, u')
+  | Construct (co, u) when not (Univ.Instance.is_empty u) ->
+    let u' = Evd.normalize_universe_instance sigma u in
+    if u' == u then c0 else Construct (co, u')
+  | App (c, args) when isEvar c ->
+    (** Enforce smart constructor invariant on applications *)
+    let ev = destEvar c in
+    begin match safe_evar_value sigma ev with
+    | None -> c0
+    | Some c -> kind sigma (mkApp (c, args))
+    end
+  | _ -> c0
+
+let kind_upto = kind
+let of_kind = Constr.of_kind
+let of_constr c = c
+let unsafe_to_constr c = c
+let unsafe_eq = Refl
+
+end
+
+include API
+
+type types = t
+type constr = t
+type existential = t pexistential
+type fixpoint = (t, t) pfixpoint
+type cofixpoint = (t, t) pcofixpoint
+
+let mkProp = of_kind (Sort Sorts.prop)
+let mkSet = of_kind (Sort Sorts.set)
+let mkType u = of_kind (Sort (Sorts.Type u))
+let mkRel n = of_kind (Rel n)
+let mkVar id = of_kind (Var id)
+let mkMeta n = of_kind (Meta n)
+let mkEvar e = of_kind (Evar e)
+let mkSort s = of_kind (Sort s)
+let mkCast (b, k, t) = of_kind (Cast (b, k, t))
+let mkProd (na, t, u) = of_kind (Prod (na, t, u))
+let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
+let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
+let mkApp (f, arg) = of_kind (App (f, arg))
+let mkConstU pc = of_kind (Const pc)
+let mkIndU pi = of_kind (Ind pi)
+let mkConstructU pc = of_kind (Construct pc)
+let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
+let mkFix f = of_kind (Fix f)
+let mkCoFix f = of_kind (CoFix f)
+let mkProj (p, c) = of_kind (Proj (p, c))
+
+let applist (f, arg) = mkApp (f, Array.of_list arg)
+
+let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
+let isVar sigma c = match kind sigma c with Var _ -> true | _ -> false
+let isInd sigma c = match kind sigma c with Ind _ -> true | _ -> false
+let isEvar sigma c = match kind sigma c with Evar _ -> true | _ -> false
+let isMeta sigma c = match kind sigma c with Meta _ -> true | _ -> false
+let isSort sigma c = match kind sigma c with Sort _ -> true | _ -> false
+let isCast sigma c = match kind sigma c with Cast _ -> true | _ -> false
+let isApp sigma c = match kind sigma c with App _ -> true | _ -> false
+let isLambda sigma c = match kind sigma c with Lambda _ -> true | _ -> false
+let isLetIn sigma c = match kind sigma c with LetIn _ -> true | _ -> false
+let isProd sigma c = match kind sigma c with Prod _ -> true | _ -> false
+let isConst sigma c = match kind sigma c with Const _ -> true | _ -> false
+let isConstruct sigma c = match kind sigma c with Construct _ -> true | _ -> false
+let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false
+let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false
+let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
+let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
+let isVarId sigma id c =
+  match kind sigma c with Var id' -> Id.equal id id' | _ -> false
+
+let destRel sigma c = match kind sigma c with
+| Rel p -> p
+| _ -> raise DestKO
+
+let destVar sigma c = match kind sigma c with
+| Var p -> p
+| _ -> raise DestKO
+
+let destInd sigma c = match kind sigma c with
+| Ind p -> p
+| _ -> raise DestKO
+
+let destEvar sigma c = match kind sigma c with
+| Evar p -> p
+| _ -> raise DestKO
+
+let destMeta sigma c = match kind sigma c with
+| Meta p -> p
+| _ -> raise DestKO
+
+let destSort sigma c = match kind sigma c with
+| Sort p -> p
+| _ -> raise DestKO
+
+let destCast sigma c = match kind sigma c with
+| Cast (c, k, t) -> (c, k, t)
+| _ -> raise DestKO
+
+let destApp sigma c = match kind sigma c with
+| App (f, a) -> (f, a)
+| _ -> raise DestKO
+
+let destLambda sigma c = match kind sigma c with
+| Lambda (na, t, c) -> (na, t, c)
+| _ -> raise DestKO
+
+let destLetIn sigma c = match kind sigma c with
+| LetIn (na, b, t, c) -> (na, b, t, c)
+| _ -> raise DestKO
+
+let destProd sigma c = match kind sigma c with
+| Prod (na, t, c) -> (na, t, c)
+| _ -> raise DestKO
+
+let destConst sigma c = match kind sigma c with
+| Const p -> p
+| _ -> raise DestKO
+
+let destConstruct sigma c = match kind sigma c with
+| Construct p -> p
+| _ -> raise DestKO
+
+let destFix sigma c = match kind sigma c with
+| Fix p -> p
+| _ -> raise DestKO
+
+let destCoFix sigma c = match kind sigma c with
+| CoFix p -> p
+| _ -> raise DestKO
+
+let destCase sigma c = match kind sigma c with
+| Case (ci, t, c, p) -> (ci, t, c, p)
+| _ -> raise DestKO
+
+let destProj sigma c = match kind sigma c with
+| Proj (p, c) -> (p, c)
+| _ -> raise DestKO
+
+let decompose_app sigma c =
+  match kind sigma c with
+    | App (f,cl) -> (f, Array.to_list cl)
+    | _ -> (c,[])
+
+let local_assum (na, t) =
+  let open Rel.Declaration in
+  LocalAssum (na, unsafe_to_constr t)
+
+let local_def (na, b, t) =
+  let open Rel.Declaration in
+  LocalDef (na, unsafe_to_constr b, unsafe_to_constr t)
+
+let decompose_lam sigma c =
+  let rec lamdec_rec l c = match kind sigma c with
+    | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
+    | Cast (c,_,_)     -> lamdec_rec l c
+    | _                -> l,c
+  in
+  lamdec_rec [] c
+
+let decompose_lam_assum sigma c =
+  let rec lamdec_rec l c =
+    match kind sigma c with
+    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) c
+    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Cast (c,_,_)      -> lamdec_rec l c
+    | _               -> l,c
+  in
+  lamdec_rec Context.Rel.empty c
+
+let decompose_lam_n_assum sigma n c =
+  if n < 0 then
+    error "decompose_lam_n_assum: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else
+      match kind sigma c with
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) n c
+      | Cast (c,_,_)      -> lamdec_rec l n c
+      | c -> error "decompose_lam_n_assum: not enough abstractions"
+  in
+  lamdec_rec Context.Rel.empty n c
+
+let decompose_lam_n_decls sigma n =
+  if n < 0 then
+    error "decompose_lam_n_decls: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else
+      match kind sigma c with
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Cast (c,_,_)      -> lamdec_rec l n c
+      | c -> error "decompose_lam_n_decls: not enough abstractions"
+  in
+  lamdec_rec Context.Rel.empty n
+
+let decompose_prod sigma c =
+  let rec proddec_rec l c = match kind sigma c with
+    | Prod (x,t,c) -> proddec_rec ((x,t)::l) c
+    | Cast (c,_,_)     -> proddec_rec l c
+    | _                -> l,c
+  in
+  proddec_rec [] c
+
+let decompose_prod_assum sigma c =
+  let rec proddec_rec l c =
+    match kind sigma c with
+    | Prod (x,t,c)  -> proddec_rec (Context.Rel.add (local_assum (x,t)) l) c
+    | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Cast (c,_,_)      -> proddec_rec l c
+    | _               -> l,c
+  in
+  proddec_rec Context.Rel.empty c
+
+let decompose_prod_n_assum sigma n c =
+  if n < 0 then
+    error "decompose_prod_n_assum: integer parameter must be positive";
+  let rec prodec_rec l n c =
+    if Int.equal n 0 then l,c
+    else
+      match kind sigma c with
+      | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Cast (c,_,_)      -> prodec_rec l n c
+      | c -> error "decompose_prod_n_assum: not enough assumptions"
+  in
+  prodec_rec Context.Rel.empty n c
+
+let existential_type sigma (evk, args) =
+  of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args))
+
+let map sigma f c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (b,k,t) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkCast (b', k, t')
+  | Prod (na,t,b) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkProd (na, t', b')
+  | Lambda (na,t,b) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkLambda (na, t', b')
+  | LetIn (na,b,t,k) ->
+      let b' = f b in
+      let t' = f t in
+      let k' = f k in
+      if b'==b && t' == t && k'==k then c
+      else mkLetIn (na, b', t', k')
+  | App (b,l) ->
+      let b' = f b in
+      let l' = Array.smartmap f l in
+      if b'==b && l'==l then c
+      else mkApp (b', l')
+  | Proj (p,t) ->
+      let t' = f t in
+      if t' == t then c
+      else mkProj (p, t')
+  | Evar (e,l) ->
+      let l' = Array.smartmap f l in
+      if l'==l then c
+      else mkEvar (e, l')
+  | Case (ci,p,b,bl) ->
+      let b' = f b in
+      let p' = f p in
+      let bl' = Array.smartmap f bl in
+      if b'==b && p'==p && bl'==bl then c
+      else mkCase (ci, p', b', bl')
+  | Fix (ln,(lna,tl,bl)) ->
+      let tl' = Array.smartmap f tl in
+      let bl' = Array.smartmap f bl in
+      if tl'==tl && bl'==bl then c
+      else mkFix (ln,(lna,tl',bl'))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let tl' = Array.smartmap f tl in
+      let bl' = Array.smartmap f bl in
+      if tl'==tl && bl'==bl then c
+      else mkCoFix (ln,(lna,tl',bl'))
+
+let map_with_binders sigma g f l c0 = match kind sigma c0 with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c0
+  | Cast (c, k, t) ->
+    let c' = f l c in
+    let t' = f l t in
+    if c' == c && t' == t then c0
+    else mkCast (c', k, t')
+  | Prod (na, t, c) ->
+    let t' = f l t in
+    let c' = f (g l) c in
+    if t' == t && c' == c then c0
+    else mkProd (na, t', c')
+  | Lambda (na, t, c) ->
+    let t' = f l t in
+    let c' = f (g l) c in
+    if t' == t && c' == c then c0
+    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 l) c in
+    if b' == b && t' == t && c' == c then c0
+    else mkLetIn (na, b', t', c')
+  | App (c, al) ->
+    let c' = f l c in
+    let al' = CArray.Fun1.smartmap f l al in
+    if c' == c && al' == al then c0
+    else mkApp (c', al')
+  | Proj (p, t) ->
+    let t' = f l t in
+    if t' == t then c0
+    else mkProj (p, t')
+  | Evar (e, al) ->
+    let al' = CArray.Fun1.smartmap f l al in
+    if al' == al then c0
+    else mkEvar (e, al')
+  | Case (ci, p, c, bl) ->
+    let p' = f l p in
+    let c' = f l c in
+    let bl' = CArray.Fun1.smartmap f l bl in
+    if p' == p && c' == c && bl' == bl then c0
+    else mkCase (ci, p', c', bl')
+  | Fix (ln, (lna, tl, bl)) ->
+    let tl' = CArray.Fun1.smartmap f l tl in
+    let l' = iterate g (Array.length tl) l in
+    let bl' = CArray.Fun1.smartmap f l' bl in
+    if tl' == tl && bl' == bl then c0
+    else mkFix (ln,(lna,tl',bl'))
+  | CoFix(ln,(lna,tl,bl)) ->
+    let tl' = CArray.Fun1.smartmap f l tl in
+    let l' = iterate g (Array.length tl) l in
+    let bl' = CArray.Fun1.smartmap f l' bl in
+    mkCoFix (ln,(lna,tl',bl'))
+
+let iter sigma f c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f c; f t
+  | Prod (_,t,c) -> f t; f c
+  | Lambda (_,t,c) -> f t; f c
+  | LetIn (_,b,t,c) -> f b; f t; f c
+  | App (c,l) -> f c; Array.iter f l
+  | Proj (p,c) -> f c
+  | Evar (_,l) -> Array.iter f l
+  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
+  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+
+let iter_with_full_binders sigma g f n c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f n c; f n t
+  | Prod (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
+  | Lambda (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
+  | LetIn (na,b,t,c) -> f n b; f n t; f (g (local_def (na, b, t)) n) c
+  | App (c,l) -> f n c; CArray.Fun1.iter f n l
+  | Evar (_,l) -> CArray.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | Proj (p,c) -> f n c
+  | Fix (_,(lna,tl,bl)) ->
+    Array.iter (f n) tl;
+    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    Array.iter (f n') bl
+  | CoFix (_,(lna,tl,bl)) ->
+    Array.iter (f n) tl;
+    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    Array.iter (f n') bl
+
+let iter_with_binders sigma g f n c =
+  iter_with_full_binders sigma (fun _ acc -> g acc) f n c
+
+let fold sigma f acc c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> acc
+  | Cast (c,_,t) -> f (f acc c) t
+  | Prod (_,t,c) -> f (f acc t) c
+  | Lambda (_,t,c) -> f (f acc t) c
+  | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+  | App (c,l) -> Array.fold_left f (f acc c) l
+  | Proj (p,c) -> f acc c
+  | Evar (_,l) -> Array.fold_left f acc l
+  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+  | CoFix (_,(lna,tl,bl)) ->
+    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+
+let to_constr sigma t =
+  let rec map c = Constr.map map (Constr.of_kind (kind_upto sigma c)) in
+  map (unsafe_to_constr t)
+
+let compare_gen k eq_inst eq_sort eq_constr c1 c2 =
+  (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2
+
+let eq_constr sigma c1 c2 =
+  let kind c = kind_upto sigma c in
+  let rec eq_constr c1 c2 =
+    compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2
+  in
+  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+let eq_constr_nounivs sigma c1 c2 =
+  let kind c = kind_upto sigma c in
+  let rec eq_constr c1 c2 =
+    compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2
+  in
+  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+(** TODO: factorize with universes.ml *)
+let test_constr_universes sigma leq m n =
+  let open Universes in
+  let kind c = kind_upto sigma c in
+  if m == n then Some Constraints.empty
+  else 
+    let cstrs = ref Constraints.empty in
+    let eq_universes strict l l' = 
+      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+    let eq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else (cstrs := Constraints.add 
+	      (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; 
+	    true)
+    in
+    let leq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else 
+	(cstrs := Constraints.add 
+	   (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; 
+	 true)
+    in
+    let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in
+    let res =
+      if leq then
+        let rec compare_leq m n =
+          Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n
+        and leq_constr' m n = m == n || compare_leq m n in
+        compare_leq m n
+      else
+        Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n
+    in
+    if res then Some !cstrs else None
+
+let eq_constr_universes sigma m n =
+  test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+let leq_constr_universes sigma m n =
+  test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+
+let compare_head_gen_proj env sigma equ eqs eqc' m n =
+  let kind c = kind_upto sigma c in
+  match kind_upto sigma m, kind_upto sigma n with
+  | Proj (p, c), App (f, args)
+  | App (f, args), Proj (p, c) -> 
+      (match kind_upto sigma f with
+      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
+          let pb = Environ.lookup_projection p env in
+          let npars = pb.Declarations.proj_npars in
+	  if Array.length args == npars + 1 then
+	    eqc' c args.(npars)
+	  else false
+      | _ -> false)
+  | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n
+
+let eq_constr_universes_proj env sigma m n =
+  let open Universes in
+  if m == n then Some Constraints.empty
+  else 
+    let cstrs = ref Constraints.empty in
+    let eq_universes strict l l' = 
+      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+    let eq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else
+	(cstrs := Constraints.add 
+	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+	 true)
+    in
+    let rec eq_constr' m n = 
+      m == n ||	compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n
+    in
+    let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
+    if res then Some !cstrs else None
+
+module Vars =
+struct
+exception LocalOccur
+let to_constr = unsafe_to_constr
+
+(** Operations that commute with evar-normalization *)
+let lift n c = of_constr (Vars.lift n (to_constr c))
+let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
+
+let substnl subst n c = of_constr (Vars.substnl (List.map to_constr subst) n (to_constr c))
+let substl subst c = of_constr (Vars.substl (List.map to_constr subst) (to_constr c))
+let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r))
+
+let replace_vars subst c =
+  let map (id, c) = (id, to_constr c) in
+  of_constr (Vars.replace_vars (List.map map subst) (to_constr c))
+let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
+let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
+let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
+
+(** Operations that dot NOT commute with evar-normalization *)
+let noccurn sigma n term =
+  let rec occur_rec n c = match kind sigma c with
+    | Rel m -> if Int.equal m n then raise LocalOccur
+    | _ -> iter_with_binders sigma succ occur_rec n c
+  in
+  try occur_rec n term; true with LocalOccur -> false
+
+let noccur_between sigma n m term =
+  let rec occur_rec n c = match kind sigma c with
+    | Rel p -> if n<=p && p<n+m then raise LocalOccur
+    | _        -> iter_with_binders sigma succ occur_rec n c
+  in
+  try occur_rec n term; true with LocalOccur -> false
+
+let closedn sigma n c =
+  let rec closed_rec n c = match kind sigma c with
+    | Rel m -> if m>n then raise LocalOccur
+    | _ -> iter_with_binders sigma succ closed_rec n c
+  in
+  try closed_rec n c; true with LocalOccur -> false
+
+let closed0 sigma c = closedn sigma 0 c
+
+end
+
+let rec isArity sigma c =
+  match kind sigma c with
+  | Prod (_,_,c)    -> isArity sigma c
+  | LetIn (_,b,_,c) -> isArity sigma (Vars.subst1 b c)
+  | Cast (c,_,_)      -> isArity sigma c
+  | Sort _          -> true
+  | _               -> false
+
+let mkProd_or_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (na,t) -> mkProd (na, of_constr t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+
+let mkLambda_or_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (na,t) -> mkLambda (na, of_constr t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+
+let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
+let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
+
+module Unsafe =
+struct
+let to_constr = unsafe_to_constr
+let eq = unsafe_eq
+end
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
new file mode 100644
index 000000000..03e2d4ffc
--- /dev/null
+++ b/engine/eConstr.mli
@@ -0,0 +1,183 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CSig
+open Names
+open Constr
+open Context
+
+type t
+(** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring
+    that {!Constr.kind} does not observe defined evars. *)
+
+type types = t
+type constr = t
+type existential = t pexistential
+type fixpoint = (t, t) pfixpoint
+type cofixpoint = (t, t) pcofixpoint
+
+(** {5 Destructors} *)
+
+val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
+(** Same as {!Constr.kind} except that it expands evars and normalizes
+    universes on the fly. *)
+
+val to_constr : Evd.evar_map -> t -> Constr.t
+(** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *)
+
+(** {5 Constructors} *)
+
+val of_kind : (t, t) Constr.kind_of_term -> t
+(** Construct a term from a view. *)
+
+val of_constr : Constr.t -> t
+(** Translate a kernel term into an incomplete term in O(1). *)
+
+(** {5 Insensitive primitives}
+
+  Evar-insensitive versions of the corresponding functions. See the {!Constr}
+  module for more information.
+
+*)
+
+(** {6 Constructors} *)
+
+val mkRel : int -> t
+val mkVar : Id.t -> t
+val mkMeta : metavariable -> t
+val mkEvar : t pexistential -> t
+val mkSort : Sorts.t -> t
+val mkProp : t
+val mkSet  : t
+val mkType : Univ.universe -> t
+val mkCast : t * cast_kind * t -> t
+val mkProd : Name.t * t * t -> t
+val mkLambda : Name.t * t * t -> t
+val mkLetIn : Name.t * t * t * t -> t
+val mkApp : t * t array -> t
+(* val mkConst : constant -> t *)
+val mkConstU : pconstant -> t
+val mkProj : (projection * t) -> t
+(* val mkInd : inductive -> t *)
+val mkIndU : pinductive -> t
+(* val mkConstruct : constructor -> t *)
+val mkConstructU : pconstructor -> t
+(* val mkConstructUi : pinductive * int -> t *)
+val mkCase : case_info * t * t * t array -> t
+val mkFix : (t, t) pfixpoint -> t
+val mkCoFix : (t, t) pcofixpoint -> t
+
+val applist : t * t list -> t
+
+val mkProd_or_LetIn : Rel.Declaration.t -> t -> t
+val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t
+val it_mkProd_or_LetIn : t -> Rel.t -> t
+val it_mkLambda_or_LetIn : t -> Rel.t -> t
+
+(** {6 Simple case analysis} *)
+
+val isRel  : Evd.evar_map -> t -> bool
+val isVar  : Evd.evar_map -> t -> bool
+val isInd  : Evd.evar_map -> t -> bool
+val isEvar : Evd.evar_map -> t -> bool
+val isMeta : Evd.evar_map -> t -> bool
+val isSort : Evd.evar_map -> t -> bool
+val isCast : Evd.evar_map -> t -> bool
+val isApp : Evd.evar_map -> t -> bool
+val isLambda : Evd.evar_map -> t -> bool
+val isLetIn : Evd.evar_map -> t -> bool
+val isProd : Evd.evar_map -> t -> bool
+val isConst : Evd.evar_map -> t -> bool
+val isConstruct : Evd.evar_map -> t -> bool
+val isFix : Evd.evar_map -> t -> bool
+val isCoFix : Evd.evar_map -> t -> bool
+val isCase : Evd.evar_map -> t -> bool
+val isProj : Evd.evar_map -> t -> bool
+val isArity : Evd.evar_map -> t -> bool
+val isVarId  : Evd.evar_map -> Id.t -> t -> bool
+
+val destRel : Evd.evar_map -> t -> int
+val destMeta : Evd.evar_map -> t -> metavariable
+val destVar : Evd.evar_map -> t -> Id.t
+val destSort : Evd.evar_map -> t -> Sorts.t
+val destCast : Evd.evar_map -> t -> t * cast_kind * t
+val destProd : Evd.evar_map -> t -> Name.t * types * types
+val destLambda : Evd.evar_map -> t -> Name.t * types * t
+val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
+val destApp : Evd.evar_map -> t -> t * t array
+val destConst : Evd.evar_map -> t -> constant puniverses
+val destEvar : Evd.evar_map -> t -> t pexistential
+val destInd : Evd.evar_map -> t -> inductive puniverses
+val destConstruct : Evd.evar_map -> t -> constructor puniverses
+val destCase : Evd.evar_map -> t -> case_info * t * t * t array
+val destProj : Evd.evar_map -> t -> projection * t
+val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
+val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
+
+val decompose_app : Evd.evar_map -> t -> t * t list
+
+val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_lam_assum : Evd.evar_map -> t -> Context.Rel.t * t
+val decompose_lam_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t
+val decompose_lam_n_decls : Evd.evar_map -> int -> t -> Context.Rel.t * t
+
+val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_prod_assum : Evd.evar_map -> t -> Context.Rel.t * t
+val decompose_prod_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t
+
+val existential_type : Evd.evar_map -> existential -> types
+
+(** {6 Equality} *)
+
+val eq_constr : Evd.evar_map -> t -> t -> bool
+val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
+val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option
+
+(** {6 Iterators} *)
+
+val map : Evd.evar_map -> (t -> t) -> t -> t
+val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
+val iter : Evd.evar_map -> (t -> unit) -> t -> unit
+val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Evd.evar_map -> (Rel.Declaration.t -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
+
+(** {6 Substitutions} *)
+
+module Vars :
+sig
+val lift : int -> t -> t
+val liftn : int -> int -> t -> t
+val substnl : t list -> int -> t -> t
+val substl : t list -> t -> t
+val subst1 : t -> t -> t
+
+val replace_vars : (Id.t * t) list -> t -> t
+val substn_vars : int -> Id.t list -> t -> t
+val subst_vars : Id.t list -> t -> t
+val subst_var : Id.t -> t -> t
+
+val noccurn : Evd.evar_map -> int -> t -> bool
+val noccur_between : Evd.evar_map -> int -> int -> t -> bool
+
+val closedn : Evd.evar_map -> int -> t -> bool
+val closed0 : Evd.evar_map -> t -> bool
+end
+
+(** {5 Unsafe operations} *)
+
+module Unsafe :
+sig
+  val to_constr : t -> Constr.t
+  (** Physical identity. Does not care for defined evars. *)
+
+  val eq : (t, Constr.t) eq
+  (** Use for transparent cast between types. *)
+end
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 53cbbd73e..c78f37a85 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,6 +4,7 @@ Universes
 UState
 Evd
 Sigma
+EConstr
 Termops
 Proofview_monad
 Evarutil
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751ab..0ae3fb474 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -235,6 +235,12 @@ let mkVar id = Var id
 
 let kind c = c
 
+(* The other way around. We treat specifically smart constructors *)
+let of_kind = function
+| App (f, a) -> mkApp (f, a)
+| Cast (c, knd, t) -> mkCast (c, knd, t)
+| k -> k
+
 (****************************************************************************)
 (*              Functions to recur through subterms                         *)
 (****************************************************************************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 7095dbe6f..c8be89fe2 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -223,6 +223,7 @@ type ('constr, 'types) kind_of_term =
    term *)
 
 val kind : constr -> (constr, types) kind_of_term
+val of_kind : (constr, types) kind_of_term -> constr
 
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
    and application grouping *)
@@ -310,6 +311,15 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
+val compare_head_gen_leq_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+
 (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
     like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
     is used,rather than {!kind}, to expose the immediate subterms of