1 files changed, 52 insertions, 30 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 6ba8a51120..62d3963954 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -13,11 +13,13 @@ open Names
 open Nameops
 open Term
 open Vars
-open Termops
 open Environ
 open Globnames
 open Context.Named.Declaration
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (** Generic filters *)
 module Filter :
 sig
@@ -226,7 +228,7 @@ let evar_instance_array test_id info args =
     if i < len then
       let c = Array.unsafe_get args i in
       if test_id d c then instrec filter ctxt (succ i)
-      else (get_id d, c) :: instrec filter ctxt (succ i)
+      else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
@@ -235,7 +237,7 @@ let evar_instance_array test_id info args =
      let map i d =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (get_id d, c)
+        if test_id d c then None else Some (NamedDecl.get_id d, c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -243,7 +245,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (isVarId % get_id) info args
+  evar_instance_array (NamedDecl.get_id %> isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -284,7 +286,7 @@ let metavars_of c =
   let rec collrec acc c =
     match kind_of_term c with
       | Meta mv -> Int.Set.add mv acc
-      | _         -> fold_constr collrec acc c
+      | _         -> Term.fold_constr collrec acc c
   in
   collrec Int.Set.empty c
 
@@ -383,8 +385,7 @@ let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
   | Misctypes.IntroAnonymous -> None
   | Misctypes.IntroIdentifier id ->
     if Idmap.mem id idtoev then
-    user_err_loc
-      (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
+    user_err  (str "Already an existential evar of name " ++ pr_id id);
     Some id
   | Misctypes.IntroFresh id ->
     let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
@@ -641,6 +642,7 @@ let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
 let add_conv_pb ?(tail=false) pb d =
+  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
@@ -679,13 +681,16 @@ let restrict evk filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (mkVar % get_id) ctxt in
+  let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }, evk'
+    defn_evars; last_mods; evar_names }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -731,23 +736,22 @@ let evar_list c =
   let rec evrec acc c =
     match kind_of_term c with
     | Evar (evk, _ as ev) -> ev :: acc
-    | _ -> fold_constr evrec acc c in
+    | _ -> Term.fold_constr evrec acc c in
   evrec [] c
 
 let evars_of_term c =
   let rec evrec acc c =
     match kind_of_term c with
     | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
-    | _ -> fold_constr evrec acc c
+    | _ -> Term.fold_constr evrec acc c
   in
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
-  List.fold_right (fun decl s ->
-    Option.fold_left (fun s t ->
-      Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl))
-    nc Evar.Set.empty
+  Context.Named.fold_outside
+    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr)))
+    nc
+    ~init:Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
   Evar.Set.union (evars_of_term evi.evar_concl)
@@ -853,6 +857,13 @@ let is_eq_sort s1 s2 =
       if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
+(* Precondition: l is not defined in the substitution *)
+let universe_rigidity evd l =
+  let uctx = evd.universes in
+  if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then
+    UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx))
+  else UnivRigid
+
 let normalize_universe evd =
   let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
@@ -1262,7 +1273,9 @@ 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 (f_print_constr, print_constr_hook) = Hook.make ()
+
+let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a
 
 let pr_meta_map mmap =
   let pr_name = function
@@ -1283,13 +1296,13 @@ let pr_meta_map mmap =
   prlist pr_meta_binding (metamap_to_list mmap)
 
 let pr_decl (decl,ok) =
-  let id = get_id decl in
-  match get_value decl with
-  | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
-  | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
-      print_constr c ++ str (if ok then ")" else "}")
+  match decl with
+  | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+  | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
+                           print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
+  | Evar_kinds.NamedHole id -> pr_id id
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
@@ -1398,12 +1411,11 @@ let pr_evar_universe_context ctx =
        h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
 
 let print_env_short env =
-  let pr_body n = function
-  | None -> pr_name n
-  | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
-  let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in
-  let pr_rel_decl decl = let open Context.Rel.Declaration in
-                         pr_body (get_name decl) (get_value decl) in
+  let pr_rel_decl = function
+    | RelDecl.LocalAssum (n,_) -> pr_name n
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+  in
+  let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
@@ -1411,12 +1423,22 @@ let print_env_short env =
 
 let pr_evar_constraints pbs =
   let pr_evconstr (pbty, env, t1, t2) =
+    let env =
+      (** We currently allow evar instances to refer to anonymous de
+          Bruijn indices, so we protect the error printing code in this
+          case by giving names to every de Bruijn variable in the
+          rel_context of the conversion problem. MS: we should rather
+          stop depending on anonymous variables, they can be used to
+          indicate independency. Also, this depends on a strategy for
+          naming/renaming. *)
+      Namegen.make_all_name_different env
+    in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env t1 ++ spc () ++
+      Hook.get f_print_constr env t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ print_constr_env env t2
+      spc () ++ Hook.get f_print_constr env t2
   in
   prlist_with_sep fnl pr_evconstr pbs