From a42795cc1c2a8ed3efa9960af920ff7b16d928f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 1 Sep 2016 17:52:44 +0200
Subject: Introducing a new EConstr.t type to perform the nf_evar operation on
 demand.

---
 kernel/constr.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751abc..0ae3fb474d 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                         *)
 (****************************************************************************)
-- 
cgit v1.2.3


From ce029533a1f0fc6ac9e28d162350a64446522246 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:05:17 +0200
Subject: Make the Constr.kind_of_term type parametric in sorts and universes.

---
 kernel/constr.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 0ae3fb474d..5a7561bf50 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -81,27 +81,27 @@ type pconstructor = constructor puniverses
 
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
-type ('constr, 'types) kind_of_term =
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
-  | Sort      of Sorts.t
+  | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
   | Prod      of Name.t * 'types * 'types
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of pconstant
-  | Ind       of pinductive
-  | Construct of pconstructor
+  | Const     of (constant * 'univs)
+  | Ind       of (inductive * 'univs)
+  | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of projection * 'constr
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
-type t = (t,t) kind_of_term
+type t = (t, t, Sorts.t, Instance.t) kind_of_term
 type constr = t
 
 type existential = existential_key * constr array
-- 
cgit v1.2.3