Merge branch 'v8.6'

7 files changed, 127 insertions, 72 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b63391913f..bd86f4bd27 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -290,78 +290,107 @@ 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 push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
+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
+
+type csubst = int * Constr.t Int.Map.t
+
+let empty_csubst = (0, Int.Map.empty)
+
+type ext_named_context =
+  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 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
     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, 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
+        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
+      (** 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) ->
+      (* 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 = (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
+      (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
+          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
+      (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 *)
+  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 *)
   (* 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)
-      )
-      (rel_context env) ~init:([], [], ids, env) in
-  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
+    Context.Rel.fold_outside push_rel_decl_to_named_context
+      (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)
 
 (*------------------------------------*
  * Entry points to define new evars   *
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 111d0f3e8c..c0c81442d5 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,8 +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 =
+  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
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 196f44760a..6ba8a51120 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 =
@@ -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"]"
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/namegen.ml b/engine/namegen.ml
index 129cb3868e..638adea5d3 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
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 ->