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.
---
 kernel/environ.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a543f1957..5688813ad6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -469,9 +469,11 @@ let lookup_modtype mp env =
 
 (*s Judgments. *)
 
-type unsafe_judgment = {
-  uj_val : constr;
-  uj_type : types }
+type ('constr, 'types) punsafe_judgment = {
+  uj_val : 'constr;
+  uj_type : 'types }
+
+type unsafe_judgment = (constr, types) punsafe_judgment
 
 let make_judge v tj =
   { uj_val = v;
@@ -480,10 +482,12 @@ let make_judge v tj =
 let j_val j = j.uj_val
 let j_type j = j.uj_type
 
-type unsafe_type_judgment = {
-  utj_val : constr;
+type 'types punsafe_type_judgment = {
+  utj_val : 'types;
   utj_type : sorts }
 
+type unsafe_type_judgment = types punsafe_type_judgment
+
 (*s Compilation of global declaration *)
 
 let compile_constant_body = Cbytegen.compile_constant_body false
-- 
cgit v1.2.3


From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 15:30:02 +0100
Subject: Introducing contexts parameterized by the inner term type.

This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
---
 kernel/environ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5688813ad6..9986f439af 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -120,7 +120,7 @@ let lookup_named = lookup_named
 let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
 
 let eq_named_context_val c1 c2 =
-   c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
+   c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2)
 
 (* A local const is evaluable if it is defined  *)
 
-- 
cgit v1.2.3