From b283c7674c4bff8ac2be52e896a40ba155c3d994 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 27 Jul 2016 09:03:42 +0200
Subject: Exporting the renaming API for evar declaration.

---
 engine/evarutil.ml  | 93 +++++++++++++++++++++++++++--------------------------
 engine/evarutil.mli |  7 ++++
 2 files changed, 54 insertions(+), 46 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b63391913f..8bba449c66 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -293,12 +293,8 @@ let make_pure_subst evi args =
 let subst2 subst vsubst c =
   substl subst (replace_vars vsubst c)
 
-let push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
+let push_rel_decl_to_named_context decl (subst, vsubst, avoid, env) =
   let open Context.Named.Declaration in
-  let ids = List.map get_id (named_context env) in
-  let inst_vars = List.map mkVar ids in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   let replace_var_named_declaration id0 id decl =
     let id' = get_id decl in
     let id' = if Id.equal id0 id' then id else id' in
@@ -315,51 +311,56 @@ let push_rel_context_to_named_context env typ =
     | Name id' when id_ord id id' = 0 -> None
     | Name id' -> Some id'
   in
+  let open Context.Rel.Declaration in
+  let na = get_name decl in
+  let c = get_value decl in
+  let t = get_type decl in
+  let open Context.Named.Declaration in
+  let id =
+    (* ppedrot: we want to infer nicer names for the refine tactic, but
+        keeping at the same time backward compatibility in other code
+        using this function. For now, we only attempt to preserve the
+        old behaviour of Program, but ultimately, one should do something
+        about this whole name generation problem. *)
+    if Flags.is_program_mode () then next_name_away na avoid
+    else next_ident_away (id_of_name_using_hdchar env t na) avoid
+  in
+  match extract_if_neq id na with
+  | Some id0 when not (is_section_variable id0) ->
+      (* spiwack: if [id<>id0], rather than introducing a new
+          binding named [id], we will keep [id0] (the name given
+          by the user) and rename [id0] into [id] in the named
+          context. Unless [id] is a section variable. *)
+      let subst = List.map (replace_vars [id0,mkVar id]) subst in
+      let vsubst = (id0,mkVar id)::vsubst in
+      let d = match c with
+        | None -> LocalAssum (id0, subst2 subst vsubst t)
+        | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
+      in
+      let env = replace_var_named_context id0  id env in
+      (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
+  | _ ->
+      (* spiwack: if [id0] is a section variable renaming it is
+          incorrect. We revert to a less robust behaviour where
+          the new binder has name [id]. Which amounts to the same
+          behaviour than when [id=id0]. *)
+      let d = match c with
+        | None -> LocalAssum (id, subst2 subst vsubst t)
+        | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
+      in
+      (mkVar id :: subst, vsubst, id::avoid, push_named d env)
+
+let push_rel_context_to_named_context env typ =
+  (* compute the instances relative to the named context and rel_context *)
+  let open Context.Named.Declaration in
+  let ids = List.map get_id (named_context env) in
+  let inst_vars = List.map mkVar ids in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   (* move the rel context to a named context and extend the named instance *)
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
-    Context.Rel.fold_outside
-      (fun decl (subst, vsubst, avoid, env) ->
-        let open Context.Rel.Declaration in
-        let na = get_name decl in
-	let c = get_value decl in
-	let t = get_type decl in
-        let open Context.Named.Declaration in
-        let id =
-          (* ppedrot: we want to infer nicer names for the refine tactic, but
-             keeping at the same time backward compatibility in other code
-             using this function. For now, we only attempt to preserve the
-             old behaviour of Program, but ultimately, one should do something
-             about this whole name generation problem. *)
-          if Flags.is_program_mode () then next_name_away na avoid
-          else next_ident_away (id_of_name_using_hdchar env t na) avoid
-        in
-        match extract_if_neq id na with
-        | Some id0 when not (is_section_variable id0) ->
-            (* spiwack: if [id<>id0], rather than introducing a new
-               binding named [id], we will keep [id0] (the name given
-               by the user) and rename [id0] into [id] in the named
-               context. Unless [id] is a section variable. *)
-            let subst = List.map (replace_vars [id0,mkVar id]) subst in
-            let vsubst = (id0,mkVar id)::vsubst in
-            let d = match c with
-              | None -> LocalAssum (id0, subst2 subst vsubst t)
-              | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-            let env = replace_var_named_context id0  id env in
-            (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
-        | _ ->
-            (* spiwack: if [id0] is a section variable renaming it is
-               incorrect. We revert to a less robust behaviour where
-               the new binder has name [id]. Which amounts to the same
-               behaviour than when [id=id0]. *)
-            let d = match c with
-              | None -> LocalAssum (id, subst2 subst vsubst t)
-              | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
-      )
+    Context.Rel.fold_outside push_rel_decl_to_named_context
       (rel_context env) ~init:([], [], ids, env) in
   (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 111d0f3e8c..a4200d762b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,6 +199,13 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
   Id.Set.t -> named_context_val * types * types
 
+val push_rel_decl_to_named_context :
+  Context.Rel.Declaration.t ->
+  Vars.substl * (Names.Id.t * Constr.constr) list *
+  Names.Id.t list * Environ.env ->
+  Term.constr list * (Names.Id.t * Constr.constr) list *
+  Names.Id.t list * Environ.env
+
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
 
-- 
cgit v1.2.3


From 62d5ef53da153394c69b52cc707b72d53eaeac44 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Aug 2016 15:32:48 +0200
Subject: Simplifying code in evar generation.

We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
---
 engine/evarutil.ml  | 26 +++++++++++---------------
 engine/evarutil.mli |  4 ++--
 2 files changed, 13 insertions(+), 17 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 8bba449c66..5be6fa8ab1 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -293,7 +293,7 @@ let make_pure_subst evi args =
 let subst2 subst vsubst c =
   substl subst (replace_vars vsubst c)
 
-let push_rel_decl_to_named_context decl (subst, vsubst, avoid, env) =
+let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
   let replace_var_named_declaration id0 id decl =
     let id' = get_id decl in
@@ -301,20 +301,13 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, env) =
     let vsubst = [id0 , mkVar id] in
     decl |> set_id id' |> map_constr (replace_vars vsubst)
   in
-  let replace_var_named_context id0 id  env =
-    let nc = Environ.named_context env in
-    let nc' = List.map (replace_var_named_declaration id0 id) nc in
-    Environ.reset_with_named_context (val_of_named_context nc') env
-  in
   let extract_if_neq id = function
     | Anonymous -> None
     | Name id' when id_ord id id' = 0 -> None
     | Name id' -> Some id'
   in
   let open Context.Rel.Declaration in
-  let na = get_name decl in
-  let c = get_value decl in
-  let t = get_type decl in
+  let (na, c, t) = to_tuple decl in
   let open Context.Named.Declaration in
   let id =
     (* ppedrot: we want to infer nicer names for the refine tactic, but
@@ -323,7 +316,10 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, env) =
         old behaviour of Program, but ultimately, one should do something
         about this whole name generation problem. *)
     if Flags.is_program_mode () then next_name_away na avoid
-    else next_ident_away (id_of_name_using_hdchar env t na) avoid
+    else
+      (** id_of_name_using_hdchar only depends on the rel context which is empty
+          here *)
+      next_ident_away (id_of_name_using_hdchar empty_env t na) avoid
   in
   match extract_if_neq id na with
   | Some id0 when not (is_section_variable id0) ->
@@ -337,8 +333,8 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, env) =
         | None -> LocalAssum (id0, subst2 subst vsubst t)
         | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
       in
-      let env = replace_var_named_context id0  id env in
-      (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
+      let nc = List.map (replace_var_named_declaration id0 id) nc in
+      (mkVar id0 :: subst, vsubst, id::avoid, d :: nc)
   | _ ->
       (* spiwack: if [id0] is a section variable renaming it is
           incorrect. We revert to a less robust behaviour where
@@ -348,7 +344,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, env) =
         | None -> LocalAssum (id, subst2 subst vsubst t)
         | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
       in
-      (mkVar id :: subst, vsubst, id::avoid, push_named d env)
+      (mkVar id :: subst, vsubst, id::avoid, d :: nc)
 
 let push_rel_context_to_named_context env typ =
   (* compute the instances relative to the named context and rel_context *)
@@ -361,8 +357,8 @@ let push_rel_context_to_named_context env typ =
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
     Context.Rel.fold_outside push_rel_decl_to_named_context
-      (rel_context env) ~init:([], [], ids, env) in
-  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
+      (rel_context env) ~init:([], [], ids, named_context env) in
+  (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
 (*------------------------------------*
  * Entry points to define new evars   *
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a4200d762b..95b8b3e0bb 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -202,9 +202,9 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty
 val push_rel_decl_to_named_context :
   Context.Rel.Declaration.t ->
   Vars.substl * (Names.Id.t * Constr.constr) list *
-  Names.Id.t list * Environ.env ->
+  Names.Id.t list * Context.Named.t ->
   Term.constr list * (Names.Id.t * Constr.constr) list *
-  Names.Id.t list * Environ.env
+  Names.Id.t list * Context.Named.t
 
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
-- 
cgit v1.2.3


From 118572b57a6f15ad4342e8a75ca0836e7896d465 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Aug 2016 18:46:05 +0200
Subject: Use sets instead of lists for names to avoid in evar generation.

---
 engine/evarutil.ml  | 16 +++++++++++++---
 engine/evarutil.mli |  8 ++++----
 2 files changed, 17 insertions(+), 7 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5be6fa8ab1..b3a886f711 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -293,6 +293,15 @@ let make_pure_subst evi args =
 let subst2 subst vsubst c =
   substl subst (replace_vars vsubst c)
 
+let next_ident_away id avoid =
+  let avoid id = Id.Set.mem id avoid in
+  next_ident_away_from id avoid
+
+let next_name_away na avoid =
+  let avoid id = Id.Set.mem id avoid in
+  let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
+  next_ident_away_from id avoid
+
 let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
   let replace_var_named_declaration id0 id decl =
@@ -334,7 +343,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
         | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
       in
       let nc = List.map (replace_var_named_declaration id0 id) nc in
-      (mkVar id0 :: subst, vsubst, id::avoid, d :: nc)
+      (mkVar id0 :: subst, vsubst, Id.Set.add id avoid, d :: nc)
   | _ ->
       (* spiwack: if [id0] is a section variable renaming it is
           incorrect. We revert to a less robust behaviour where
@@ -344,12 +353,13 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
         | None -> LocalAssum (id, subst2 subst vsubst t)
         | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
       in
-      (mkVar id :: subst, vsubst, id::avoid, d :: nc)
+      (mkVar id :: subst, vsubst, Id.Set.add id avoid, d :: nc)
 
 let push_rel_context_to_named_context env typ =
   (* compute the instances relative to the named context and rel_context *)
   let open Context.Named.Declaration in
   let ids = List.map get_id (named_context env) in
+  let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
   let inst_vars = List.map mkVar ids in
   let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   (* move the rel context to a named context and extend the named instance *)
@@ -357,7 +367,7 @@ let push_rel_context_to_named_context env typ =
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
     Context.Rel.fold_outside push_rel_decl_to_named_context
-      (rel_context env) ~init:([], [], ids, named_context env) in
+      (rel_context env) ~init:([], [], avoid, named_context env) in
   (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
 (*------------------------------------*
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 95b8b3e0bb..45f0d6b078 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -201,10 +201,10 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty
 
 val push_rel_decl_to_named_context :
   Context.Rel.Declaration.t ->
-  Vars.substl * (Names.Id.t * Constr.constr) list *
-  Names.Id.t list * Context.Named.t ->
-  Term.constr list * (Names.Id.t * Constr.constr) list *
-  Names.Id.t list * Context.Named.t
+  Vars.substl * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t ->
+  Term.constr list * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t
 
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
-- 
cgit v1.2.3


From 26e5194bc252e4ac71c74f8ac73a0e2cbe82edf6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Aug 2016 19:18:48 +0200
Subject: Using the extended contexts in pretyping.

In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
---
 engine/evarutil.ml  | 4 ++++
 engine/evarutil.mli | 8 ++++----
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b3a886f711..b3e17fa9d2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -302,6 +302,10 @@ let next_name_away na avoid =
   let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
   next_ident_away_from id avoid
 
+type ext_named_context =
+  Vars.substl * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t
+
 let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
   let replace_var_named_declaration id0 id decl =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 45f0d6b078..429ea73de1 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,13 +199,13 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
   Id.Set.t -> named_context_val * types * types
 
-val push_rel_decl_to_named_context :
-  Context.Rel.Declaration.t ->
+type ext_named_context =
   Vars.substl * (Id.t * Constr.constr) list *
-  Id.Set.t * Context.Named.t ->
-  Term.constr list * (Id.t * Constr.constr) list *
   Id.Set.t * Context.Named.t
 
+val push_rel_decl_to_named_context :
+  Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
+
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
 
-- 
cgit v1.2.3


From f1e1b7f735c8cd4a1f3cc52e7f9a7cdf1481ffe5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 5 Aug 2016 12:38:12 +0200
Subject: Using a dedicated kind of substitutions in evar name generation.

This saves a quadratic allocation by replacing arrays with maps.
---
 engine/evarutil.ml  | 30 ++++++++++++++++++++++++------
 engine/evarutil.mli |  9 +++++++--
 2 files changed, 31 insertions(+), 8 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b3e17fa9d2..bd86f4bd27 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -290,8 +290,18 @@ let make_pure_subst evi args =
  *   we have the property that u and phi(t) are convertible in env.
  *)
 
+let csubst_subst (k, s) c =
+  let rec subst n c = match Constr.kind c with
+  | Rel m ->
+    if m <= n then c
+    else if m - n <= k then Int.Map.find (k - m + n) s
+    else mkRel (m - k)
+  | _ -> Constr.map_with_binders succ subst n c
+  in
+  if k = 0 then c else subst 0 c
+
 let subst2 subst vsubst c =
-  substl subst (replace_vars vsubst c)
+  csubst_subst subst (replace_vars vsubst c)
 
 let next_ident_away id avoid =
   let avoid id = Id.Set.mem id avoid in
@@ -302,10 +312,18 @@ let next_name_away na avoid =
   let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
   next_ident_away_from id avoid
 
+type csubst = int * Constr.t Int.Map.t
+
+let empty_csubst = (0, Int.Map.empty)
+
 type ext_named_context =
-  Vars.substl * (Id.t * Constr.constr) list *
+  csubst * (Id.t * Constr.constr) list *
   Id.Set.t * Context.Named.t
 
+let push_var id (n, s) =
+  let s = Int.Map.add n (mkVar id) s in
+  (succ n, s)
+
 let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
   let replace_var_named_declaration id0 id decl =
@@ -340,14 +358,14 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
           binding named [id], we will keep [id0] (the name given
           by the user) and rename [id0] into [id] in the named
           context. Unless [id] is a section variable. *)
-      let subst = List.map (replace_vars [id0,mkVar id]) subst in
+      let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in
       let vsubst = (id0,mkVar id)::vsubst in
       let d = match c with
         | None -> LocalAssum (id0, subst2 subst vsubst t)
         | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
       in
       let nc = List.map (replace_var_named_declaration id0 id) nc in
-      (mkVar id0 :: subst, vsubst, Id.Set.add id avoid, d :: nc)
+      (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc)
   | _ ->
       (* spiwack: if [id0] is a section variable renaming it is
           incorrect. We revert to a less robust behaviour where
@@ -357,7 +375,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
         | None -> LocalAssum (id, subst2 subst vsubst t)
         | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
       in
-      (mkVar id :: subst, vsubst, Id.Set.add id avoid, d :: nc)
+      (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
 
 let push_rel_context_to_named_context env typ =
   (* compute the instances relative to the named context and rel_context *)
@@ -371,7 +389,7 @@ let push_rel_context_to_named_context env typ =
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
     Context.Rel.fold_outside push_rel_decl_to_named_context
-      (rel_context env) ~init:([], [], avoid, named_context env) in
+      (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in
   (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
 (*------------------------------------*
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 429ea73de1..c0c81442d5 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,15 +199,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
   Id.Set.t -> named_context_val * types * types
 
+type csubst
+
+val empty_csubst : csubst
+val csubst_subst : csubst -> Constr.t -> Constr.t
+
 type ext_named_context =
-  Vars.substl * (Id.t * Constr.constr) list *
+  csubst * (Id.t * Constr.constr) list *
   Id.Set.t * Context.Named.t
 
 val push_rel_decl_to_named_context :
   Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
 
 val push_rel_context_to_named_context : Environ.env -> types ->
-  named_context_val * types * constr list * constr list * (identifier*constr) list
+  named_context_val * types * constr list * csubst * (identifier*constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
-- 
cgit v1.2.3


From 90303e38d22479105927f0dd2fe95cce9447bd44 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 10 Aug 2016 11:26:30 +0200
Subject: Remove unused optional "predicative" argument.

---
 engine/evd.ml    |  8 ++++----
 engine/evd.mli   |  6 +++---
 engine/sigma.ml  | 12 ++++++------
 engine/sigma.mli |  6 +++---
 4 files changed, 16 insertions(+), 16 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 196f44760a..e4b174bcb3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -790,16 +790,16 @@ let merge_universe_subst evd subst =
 let with_context_set ?loc rigid d (a, ctx) =
   (merge_context_set ?loc rigid d ctx, a)
 
-let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd =
+let new_univ_level_variable ?loc ?name rigid evd =
   let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?loc ?name ?(predicative=true) rigid evd =
+let new_univ_variable ?loc ?name rigid evd =
   let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?loc ?name ?(predicative=true) rigid d =
-  let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in
+let new_sort_variable ?loc ?name rigid d =
+  let (d', u) = new_univ_variable ?loc rigid ?name d in
     (d', Type u)
 
 let add_global_univ d u =
diff --git a/engine/evd.mli b/engine/evd.mli
index d6cf83525c..9424145113 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -508,9 +508,9 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 											   
diff --git a/engine/sigma.ml b/engine/sigma.ml
index c7b0bb5a50..9381a33af1 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,16 +36,16 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
-let new_univ_level_variable ?loc ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in
+let new_univ_level_variable ?loc ?name rigid sigma =
+  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in
   Sigma (u, sigma, ())
 
-let new_univ_variable ?loc ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in
+let new_univ_variable ?loc ?name rigid sigma =
+  let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in
   Sigma (u, sigma, ())
 
-let new_sort_variable ?loc ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in
+let new_sort_variable ?loc ?name rigid sigma =
+  let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in
   Sigma (u, sigma, ())
 
 let fresh_sort_in_family ?loc ?rigid env sigma s =
diff --git a/engine/sigma.mli b/engine/sigma.mli
index aaf603efd8..7473a251b7 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -68,11 +68,11 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string ->
   Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+val new_univ_variable : ?loc:Loc.t -> ?name:string ->
   Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+val new_sort_variable : ?loc:Loc.t -> ?name:string ->
   Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
 
 val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->
-- 
cgit v1.2.3


From 5cd253c4d8e046d7eac108b48be2d510c114a49a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 6 Aug 2016 17:46:01 +0200
Subject: Fixing printing in debugger (no global env in debugger).

---
 engine/namegen.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index bc04e3e483..84eb986845 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -191,18 +191,26 @@ let visible_ids (nenv, c) =
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
     if not (Refset_env.mem g gseen) then
+      begin
+      try
       let gseen = Refset_env.add g gseen in
       let short = shortest_qualid_of_global Id.Set.empty g in
       let dir, id = repr_qualid short in
       let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
       accu := (gseen, vseen, ids)
+      with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> ()
+      end
   | Rel p ->
     let (gseen, vseen, ids) = !accu in
     if p > n && not (Int.Set.mem p vseen) then
       let vseen = Int.Set.add p vseen in
       let name =
         try Some (lookup_name_of_rel (p - n) nenv)
-        with Not_found -> None (* Unbound indice : may happen in debug *)
+        with Not_found ->
+          (* Unbound index: may happen in debug and actually also
+             while computing temporary implicit arguments of an
+             inductive type *)
+          None
       in
       let ids = match name with
       | Some (Name id) -> Id.Set.add id ids
-- 
cgit v1.2.3


From 979b7cbba63f6c033bab40ad5c552572ab5d7d71 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 31 Jul 2016 07:57:13 +0200
Subject: Two protections against failures when printing evar_map.

Delimit the scope of the failure to ease potential need for debugging
the debugging printer.

Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
---
 engine/evd.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index e4b174bcb3..6ba8a51120 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1258,6 +1258,12 @@ let pr_instance_status (sc,typ) =
   | TypeProcessed -> str " [type is checked]"
   end
 
+let protect f x =
+  try f x
+  with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+
+let print_constr a = protect print_constr a
+
 let pr_meta_map mmap =
   let pr_name = function
       Name id -> str"[" ++ pr_id id ++ str"]"
-- 
cgit v1.2.3