From 8d69323dff6e1afd17a13dfa8a980e76acb44cdc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:35 +0200
Subject: Documenting how the recursive indices of a fixpoint are computed.

Also documenting how the implicit arguments by position are computed.
---
 kernel/constr.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751abc..d0c580d138 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,7 +107,16 @@ type constr = t
 type existential = existential_key * constr array
 type rec_declaration = Name.t array * constr array * constr array
 type fixpoint = (int array * int) * rec_declaration
+  (* The array of [int]'s tells for each component of the array of
+     mutual fixpoints the number of lambdas to skip before finding the
+     recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+     (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+     the recursive argument);
+     The second component [int] tells which component of the block is
+     returned *)
 type cofixpoint = int * rec_declaration
+  (* The component [int] tells which component of the block of
+     cofixpoint is returned *)
 
 type types = constr
 
-- 
cgit v1.2.3


From fe99efdbe409e47f20776c62a76d4de7f0188afc Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 11 Apr 2017 12:46:23 +0200
Subject: Update various comments to use "template polymorphism"

Also remove obvious comments.
---
 kernel/subtyping.ml | 2 +-
 kernel/typeops.ml   | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c8ceb064d5..d0fdf9fdae 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -117,7 +117,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name env t1 t2 =
 
-    (* Due to sort-polymorphism in inductive types, the conclusions of
+    (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
        of the types of the constructors.
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7d9a2aac09..dbc0dcb73e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -367,15 +367,13 @@ let rec execute env cstr =
 	let ft =
 	  match kind_of_term f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
-	      (* Template sort-polymorphism of inductive types *)
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_inductive_knowing_parameters env ind args
 	  | Const cst when Environ.template_polymorphic_pconstant cst env ->
-	      (* Template sort-polymorphism of constants *)
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_constant_knowing_parameters env cst args
 	  | _ ->
-	    (* Full or no sort-polymorphism *)
+	    (* No template polymorphism *)
             execute env f
 	in
 
-- 
cgit v1.2.3


From 6795bc07f53a842bcec76ad0329d0b4444a625ab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 2 Apr 2017 21:22:55 +0200
Subject: Replacing costly merges in UGraph.

---
 kernel/uGraph.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 4884d0deb1..6971c0a2b6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -354,13 +354,15 @@ let get_new_edges g to_merge =
       UMap.empty to_merge
   in
   let ltle =
-    UMap.fold (fun _ n acc ->
-      UMap.merge (fun _ strict1 strict2 ->
-        match strict1, strict2 with
-        | Some true, _ | _, Some true -> Some true
-        | _, _ -> Some false)
-        acc n.ltle)
-      to_merge_lvl UMap.empty
+    let fold _ n acc =
+      let fold u strict acc =
+        if strict then UMap.add u strict acc
+        else if UMap.mem u acc then acc
+        else UMap.add u false acc
+      in
+      UMap.fold fold n.ltle acc
+    in
+    UMap.fold fold to_merge_lvl UMap.empty
   in
   let ltle, _ = clean_ltle g ltle in
   let ltle =
-- 
cgit v1.2.3


From 051f2c1be929a46a0713b47b072bb5be0a7558d0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 24 Mar 2017 15:50:21 +0100
Subject: Fast path when checking equality of universe levels in UState.

We export the relevant level equality function in UGraph which is way faster
than checking that each one is smaller than the other as universes.
---
 kernel/uGraph.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e95cf4d1cb..ed52832fa4 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -17,6 +17,7 @@ type universes = t
 type 'a check_function = universes -> 'a -> 'a -> bool
 val check_leq : universe check_function
 val check_eq : universe check_function
+val check_eq_level : universe_level check_function
 
 (** The empty graph of universes *)
 val empty_universes : universes
-- 
cgit v1.2.3


From 34d8de84ceb853c98bc80a0623f9afeae317d75f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:25:49 +0200
Subject: Locally disable some warnings.

---
 kernel/nativecode.ml   | 2 ++
 kernel/nativelambda.ml | 3 +++
 kernel/nativevalues.ml | 3 ++-
 3 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d9659d6813..ba80ff590d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -16,6 +16,8 @@ open Nativeinstr
 open Nativelambda
 open Pre_env
 
+[@@@ocaml.warning "-32-37"]
+
 (** This file defines the mllambda code generation phase of the native
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 366f9a0a6d..fcb75c661e 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -16,6 +16,9 @@ open Nativeinstr
 
 module RelDecl = Context.Rel.Declaration
 
+(* I'm not messing with this stuff. *)
+[@@@ocaml.warning "-32"]
+
 (** This file defines the lambda code generation phase of the native compiler *)
 
 exception NotClosed
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 965ed67b07..8d5f6388cb 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -334,6 +334,7 @@ let l_or accu x y =
   if is_int x && is_int y then no_check_l_or x y
   else accu x y
 
+[@@@ocaml.warning "-37"]
 type coq_carry = 
   | Caccu of t
   | C0 of t
@@ -430,7 +431,7 @@ let addmuldiv accu x y z =
   if is_int x && is_int y && is_int z then no_check_addmuldiv x y z
   else accu x y z
 
-
+[@@@ocaml.warning "-34"]
 type coq_bool =
   | Baccu of t
   | Btrue
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 kernel/reduction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cd975ee9a9..ba714ada20 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -487,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
         if eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_instances false u1 u2 cuniv in
+	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
              convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
 	if Int.equal j1 j2 && eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_instances false u1 u2 cuniv in
+	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 	  
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 kernel/names.ml   | 2 --
 kernel/uGraph.mli | 3 +++
 kernel/univ.ml    | 4 ----
 3 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 5c10badbec..811b4a62a5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -542,7 +542,6 @@ module KerPair = struct
   end
 
   module SyntacticOrd = struct
-    type t = kernel_pair
     let compare x y = match x, y with
       | Same knx, Same kny -> KerName.compare knx kny
       | Dual (knux,kncx), Dual (knuy,kncy) ->
@@ -865,7 +864,6 @@ struct
   let hash (c, b) = (if b then 0 else 1) + Constant.hash c
 
   module SyntacticOrd = struct
-    type t = constant * bool
     let compare (c, b) (c', b') =
       if b = b' then Constant.SyntacticOrd.compare c c' else -1
     let equal (c, b as x) (c', b' as x') =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e95cf4d1cb..c8ac7df5c6 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -61,3 +61,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
 val dump_universes :
   (constraint_type -> string -> string -> unit) ->
   universes -> unit
+
+(** {6 Debugging} *)
+val check_universes_invariants : universes -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09f884ecd0..afe9cbe8d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -440,10 +440,6 @@ struct
     let set = make Level.set
     let type1 = hcons (Level.set, 1)
 
-    let is_prop = function
-      | (l,0) -> Level.is_prop l
-      | _ -> false
-	
     let is_small = function
       | (l,0) -> Level.is_small l
       | _ -> false
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 kernel/constr.ml | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf50..71efe90322 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -978,28 +978,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash)
 
 let case_info_hash = CaseinfoHash.hash
 
-module Hsorts =
-  Hashcons.Make(
-    struct
-      open Sorts
-
-      type t = Sorts.t
-      type u = universe -> universe
-      let hashcons huniv = function
-          Prop c -> Prop c
-        | Type u -> Type (huniv u)
-      let eq s1 s2 =
-        s1 == s2 ||
-	  match (s1,s2) with
-            (Prop c1, Prop c2) -> c1 == c2
-          | (Type u1, Type u2) -> u1 == u2
-          |_ -> false
-      let hash = function
-	| Prop Null -> 0 | Prop Pos -> 1
-	| Type u -> 2 + Universe.hash u
-    end)
-
-(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
 
 let hcons =
-- 
cgit v1.2.3


From 5365971dfdf4136586527aa4f4c85fbfebeee0bd Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 15:00:56 +0200
Subject: Fix for bug 5507. Mispelt de Bruijn.

---
 kernel/constr.ml  | 2 +-
 kernel/constr.mli | 2 +-
 kernel/term.ml    | 2 +-
 kernel/term.mli   | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2630c3f08..49e17d74d5 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -124,7 +124,7 @@ type types = constr
 (* Term constructors *)
 (*********************)
 
-(* Constructs a DeBrujin index with number n *)
+(* Constructs a DeBruijn index with number n *)
 let rels =
   [|Rel  1;Rel  2;Rel  3;Rel  4;Rel  5;Rel  6;Rel  7; Rel  8;
     Rel  9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 700c235e6a..d90afea8f2 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -70,7 +70,7 @@ type types = constr
 
 (** {6 Term constructors. } *)
 
-(** Constructs a DeBrujin index (DB indices begin at 1) *)
+(** Constructs a DeBruijn index (DB indices begin at 1) *)
 val mkRel : int -> constr
 
 (** Constructs a Variable *)
diff --git a/kernel/term.ml b/kernel/term.ml
index e5a681375d..7c6136f088 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -169,7 +169,7 @@ let hcons_types = Constr.hcons
 
 exception DestKO
 
-(* Destructs a DeBrujin index *)
+(* Destructs a DeBruijn index *)
 let destRel c = match kind_of_term c with
   | Rel n -> n
   | _ -> raise DestKO
diff --git a/kernel/term.mli b/kernel/term.mli
index a9bb677050..623d2c8a6b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -127,7 +127,7 @@ val is_small : sorts -> bool
 
 exception DestKO
 
-(** Destructs a DeBrujin index *)
+(** Destructs a DeBruijn index *)
 val destRel : constr -> int
 
 (** Destructs an existential variable *)
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 kernel/constr.ml     | 2 +-
 kernel/constr.mli    | 2 +-
 kernel/nativeconv.ml | 2 +-
 kernel/term.ml       | 2 +-
 kernel/term.mli      | 2 +-
 kernel/vars.ml       | 2 +-
 kernel/vars.mli      | 4 ++--
 7 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 49e17d74d5..ae58fd068b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -124,7 +124,7 @@ type types = constr
 (* Term constructors *)
 (*********************)
 
-(* Constructs a DeBruijn index with number n *)
+(* Constructs a de Bruijn index with number n *)
 let rels =
   [|Rel  1;Rel  2;Rel  3;Rel  4;Rel  5;Rel  6;Rel  7; Rel  8;
     Rel  9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
diff --git a/kernel/constr.mli b/kernel/constr.mli
index d90afea8f2..e0954160f9 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -70,7 +70,7 @@ type types = constr
 
 (** {6 Term constructors. } *)
 
-(** Constructs a DeBruijn index (DB indices begin at 1) *)
+(** Constructs a de Bruijn index (DB indices begin at 1) *)
 val mkRel : int -> constr
 
 (** Constructs a Variable *)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3c0afe3805..3593d94c2c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -141,7 +141,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        (* TODO change 0 when we can have deBruijn *)
+        (* TODO change 0 when we can have de Bruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
diff --git a/kernel/term.ml b/kernel/term.ml
index 7c6136f088..03562d9f31 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -169,7 +169,7 @@ let hcons_types = Constr.hcons
 
 exception DestKO
 
-(* Destructs a DeBruijn index *)
+(* Destructs a de Bruijn index *)
 let destRel c = match kind_of_term c with
   | Rel n -> n
   | _ -> raise DestKO
diff --git a/kernel/term.mli b/kernel/term.mli
index 623d2c8a6b..241ef322fa 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -127,7 +127,7 @@ val is_small : sorts -> bool
 
 exception DestKO
 
-(** Destructs a DeBruijn index *)
+(** Destructs a de Bruijn index *)
 val destRel : constr -> int
 
 (** Destructs an existential variable *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4affb5f9fb..f1c0a4f08a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -27,7 +27,7 @@ let closedn n c =
   in
   try closed_rec n c; true with LocalOccur -> false
 
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
 
 let closed0 c = closedn 0 c
 
diff --git a/kernel/vars.mli b/kernel/vars.mli
index adeac422e0..df5c55118f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -11,10 +11,10 @@ open Constr
 
 (** {6 Occur checks } *)
 
-(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *)
 val closedn : int -> constr -> bool
 
-(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
 val closed0 : constr -> bool
 
 (** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M]  *)
-- 
cgit v1.2.3


From ba9806a242c7ece41a93181d1fb91279c89794ed Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 2 May 2017 16:10:19 +0200
Subject: Remove dead code in native compiler.

---
 kernel/nativecode.ml   | 12 -------
 kernel/nativelambda.ml | 93 --------------------------------------------------
 2 files changed, 105 deletions(-)

(limited to 'kernel')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ba80ff590d..5130aa9a4a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -42,8 +42,6 @@ module LNset = Set.Make(LNord)
 
 let lname_ctr = ref (-1)
 
-let reset_lname = lname_ctr := -1
-
 let fresh_lname n = 
   incr lname_ctr;
   { lname = n; luid = !lname_ctr }
@@ -112,40 +110,30 @@ let gname_hash gn = match gn with
 
 let case_ctr = ref (-1)
 
-let reset_gcase () = case_ctr := -1
-
 let fresh_gcase l =
   incr case_ctr;
   Gcase (l,!case_ctr)
 
 let pred_ctr = ref (-1)
 
-let reset_gpred () = pred_ctr := -1
-
 let fresh_gpred l = 
   incr pred_ctr;
   Gpred (l,!pred_ctr)
 
 let fixtype_ctr = ref (-1)
 
-let reset_gfixtype () = fixtype_ctr := -1
-
 let fresh_gfixtype l =
   incr fixtype_ctr;
   Gfixtype (l,!fixtype_ctr)
 
 let norm_ctr = ref (-1)
 
-let reset_norm () = norm_ctr := -1
-
 let fresh_gnorm l =
   incr norm_ctr;
   Gnorm (l,!norm_ctr)
 
 let normtbl_ctr = ref (-1)
 
-let reset_normtbl () = normtbl_ctr := -1
-
 let fresh_gnormtbl l =
   incr normtbl_ctr;
   Gnormtbl (l,!normtbl_ctr)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index fcb75c661e..72d9c48513 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -16,10 +16,6 @@ open Nativeinstr
 
 module RelDecl = Context.Rel.Declaration
 
-(* I'm not messing with this stuff. *)
-[@@@ocaml.warning "-32"]
-
-(** This file defines the lambda code generation phase of the native compiler *)
 
 exception NotClosed
 
@@ -164,10 +160,6 @@ let rec lam_exsubst subst lam =
   | Lrel(id,i) -> lam_subst_rel lam id i subst
   | _ -> map_lam_with_binders liftn lam_exsubst subst lam
 
-let lam_subst subst lam =
-  if is_subs_id subst then lam
-  else lam_exsubst subst lam
-
 let lam_subst_args subst args =
   if is_subs_id subst then args 
   else Array.smartmap (lam_exsubst subst) args
@@ -281,71 +273,6 @@ and reduce_lapp substf lids body substa largs =
       Llam(Array.of_list lids,  simplify (liftn (List.length lids) substf) body)
   | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
 
-
-(* [occurrence kind k lam]:
-   If [kind] is [true] return [true] if the variable [k] does not appear in 
-   [lam], return [false] if the variable appear one time and not
-   under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
-   If [kind] is [false] return [false] if the variable does not appear in [lam]
-   else raise [Not_found]
-*)
-
-let rec occurrence k kind lam =
-  match lam with
-  | Lrel (_,n) -> 
-      if Int.equal n k then 
-	if kind then false else raise Not_found
-      else kind
-  | Lvar _  | Lconst _  | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
-  | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
-  | Lprod(dom, codom) ->
-      occurrence k (occurrence k kind dom) codom
-  | Llam(ids,body) ->
-      let _ = occurrence (k+Array.length ids) false body in kind
-  | Llet(_,def,body) ->
-      occurrence (k+1) (occurrence k kind def) body
-  | Lapp(f, args) ->
-      occurrence_args k (occurrence k kind f) args
-  | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
-      occurrence_args k kind args
-  | Lcase(_,t,a,br) ->
-      let kind = occurrence k (occurrence k kind t) a in
-      let r = ref kind in
-      Array.iter (fun (_,ids,c) -> 
-	r := occurrence (k+Array.length ids) kind c && !r) br;
-      !r 
-  | Lif (t, bt, bf) ->
-      let kind = occurrence k kind t in
-      kind && occurrence k kind bt && occurrence k kind bf
-  | Lfix(_,(ids,ltypes,lbodies)) 
-  | Lcofix(_,(ids,ltypes,lbodies)) ->
-      let kind = occurrence_args k kind ltypes in
-      let _ = occurrence_args (k+Array.length ids) false lbodies in
-      kind 
-
-and occurrence_args k kind args =
-  Array.fold_left (occurrence k) kind args
-    
-let occur_once lam = 
-  try let _ = occurrence 1 true lam in true
-  with Not_found -> false
-      
-(* [remove_let lam] remove let expression in [lam] if the variable is *)
-(* used at most once time in the body, and does not appear under      *)
-(* a lambda or a fix or a cofix                                       *)
-      
-let rec remove_let subst lam =
-  match lam with
-  | Lrel(id,i) -> lam_subst_rel lam id i subst 
-  | Llet(id,def,body) ->
-      let def' = remove_let subst def in
-      if occur_once body then remove_let (cons def' subst) body
-      else 
-	let body' = remove_let (lift subst) body in
-	if def == def' && body == body' then lam else Llet(id,def',body')
-  | _ -> map_lam_with_binders liftn remove_let subst lam
-
-
 (*s Translation from [constr] to [lambda] *)
 
 (* Translation of constructor *)
@@ -410,8 +337,6 @@ module Vect =
       size = 0;
     }
 
-    let length v = v.size
-
     let extend v =
       if Int.equal v.size (Array.length v.elems) then 
 	let new_size = min (2*v.size) Sys.max_array_length in
@@ -425,33 +350,15 @@ module Vect =
       v.elems.(v.size) <- a;
       v.size <- v.size + 1
 
-    let push_pos v a =
-      let pos = v.size in
-      push v a;
-      pos
-
     let popn v n =
       v.size <- max 0 (v.size - n)
 
     let pop v = popn v 1
 	
-    let get v n =
-      if v.size <= n then invalid_arg "Vect.get:index out of bounds";
-      v.elems.(n)
-
     let get_last v n =
       if v.size <= n then invalid_arg "Vect.get:index out of bounds";
       v.elems.(v.size - n - 1)
 
-
-    let last v =
-      if Int.equal v.size 0 then invalid_arg "Vect.last:index out of bounds";
-      v.elems.(v.size - 1)
-
-    let clear v = v.size <- 0
-
-    let to_array v = Array.sub v.elems 0 v.size
-      
   end
 
 let empty_args = [||]
-- 
cgit v1.2.3


From 5b218f87bd59cfe9d510410c9acf78b5485391e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 May 2017 15:01:15 +0200
Subject: Revised behavior on ill-formed identifiers.

Namely: Replacing (currently deactivated) warning on illegal ident by
an error in strict mode and nothing in soft mode.
---
 kernel/names.ml  | 18 +++++-------------
 kernel/names.mli |  5 +++--
 2 files changed, 8 insertions(+), 15 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 811b4a62a5..f5b3f4e007 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,16 +34,8 @@ struct
 
   let hash = String.hash
 
-  let warn_invalid_identifier =
-    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
-                     ~default:CWarnings.Disabled
-                     (fun s -> str s)
-
-  let check_soft ?(warn = true) x =
-    let iter (fatal, x) =
-      if fatal then CErrors.error x else
-        if warn then warn_invalid_identifier x
-    in
+  let check_valid ?(strict=true) x =
+    let iter (fatal, x) = if fatal || strict then CErrors.error x in
     Option.iter iter (Unicode.ident_refutation x)
 
   let is_valid s = match Unicode.ident_refutation s with
@@ -52,15 +44,15 @@ struct
 
   let of_bytes s =
     let s = Bytes.to_string s in
-    check_soft s;
+    check_valid s;
     String.hcons s
 
   let of_string s =
-    let () = check_soft s in
+    let () = check_valid s in
     String.hcons s
 
   let of_string_soft s =
-    let () = check_soft ~warn:false s in
+    let () = check_valid ~strict:false s in
     String.hcons s
 
   let to_string id = id
diff --git a/kernel/names.mli b/kernel/names.mli
index be9b9422b7..5b0163aa55 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,11 +46,12 @@ sig
   val of_bytes : bytes -> t
   val of_string : string -> t
   (** Converts a string into an identifier.
-      @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
+      @raise UserError if the string is invalid as an identifier.
       @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val of_string_soft : string -> t
-  (** Same as {!of_string} except that no warning is ever issued.
+  (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted.
+      @raise UserError if the string is invalid as an UTF-8 string.
       @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val to_string : t -> string
-- 
cgit v1.2.3