From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 27 Oct 2017 14:03:51 +0200
Subject: Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
---
 interp/constrintern.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7f1dc70d95..b4c570d444 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1020,6 +1020,7 @@ let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option
 
 let glob_sort_of_level (level: glob_level) : glob_sort =
   match level with
+  | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
   | GType info -> GType [sort_info_of_level_info info]
-- 
cgit v1.2.3


From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 interp/constrintern.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b4c570d444..5ede9d6a99 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -16,6 +16,7 @@ open Names
 open Nameops
 open Namegen
 open Constr
+open Context
 open Libnames
 open Globnames
 open Impargs
@@ -2183,7 +2184,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                     (add_name match_acc CAst.(make ?loc x)) (CAst.make ?loc x::var_acc)
                 | _ ->
                   let fresh =
-                    Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
+                    Namegen.next_name_away_with_default_using_types "iV" cano_name.binder_name forbidden_names (EConstr.of_constr ty) in
                   canonize_args t tt (Id.Set.add fresh forbidden_names)
                     ((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc)
                 end
@@ -2432,9 +2433,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
        in
        let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in
 	match b with
-	    None ->
-	      let d = LocalAssum (na,t) in
-	      let impls =
+          None ->
+              let r = Retyping.relevance_of_type env sigma t in
+              let d = LocalAssum (make_annot na r,t) in
+              let impls =
 		if k == Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
 		    (ExplByPos (n, na), (true, true, true)) :: impls
@@ -2443,7 +2445,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
                 (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
               let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
-	      let d = LocalDef (na, c, t) in
+              let r = Retyping.relevance_of_type env sigma t in
+              let d = LocalDef (make_annot na r, c, t) in
                 (push_rel d env, sigma, d::params, n, impls))
       (env,sigma,[],k+1,[]) (List.rev bl)
   in sigma, ((env, par), impls)
-- 
cgit v1.2.3