Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

8 files changed, 40 insertions, 23 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8d09cbd7..9c9f6a57 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -190,7 +190,9 @@ and eval_to_patch env (buff,pl,fv) =
 and val_of_constr env c =
   let (_,fun_code,_ as ccfv) =
     try compile env c
-    with e -> print_string "can not compile \n";Format.print_flush();raise e in
+    with reraise ->
+      print_string "can not compile \n";Format.print_flush();raise reraise
+  in
   eval_to_patch env (to_memory ccfv)
 
 let set_transparent_const kn =
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 15a48e1c..9aeaf110 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -83,13 +83,14 @@ let string_of_hint = function
   | Equiv kn -> string_of_kn kn
 
 let debug_string_of_delta resolve =
-  let kn_to_string kn hint s =
-    s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint)
+  let kn_to_string kn hint l =
+    (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l
   in
-  let mp_to_string mp mp' s =
-    s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp')
+  let mp_to_string mp mp' l =
+    (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l
   in
-  Deltamap.fold mp_to_string kn_to_string resolve ""
+  let l = Deltamap.fold mp_to_string kn_to_string resolve [] in
+  String.concat ", " (List.rev l)
 
 let list_contents sub =
   let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
@@ -173,7 +174,7 @@ let solve_delta_kn resolve kn =
 
 let kn_of_delta resolve kn =
   try solve_delta_kn resolve kn
-  with _ -> kn
+  with e when Errors.noncritical e -> kn
 
 let constant_of_delta_kn resolve kn =
   constant_of_kn_equiv kn (kn_of_delta resolve kn)
@@ -182,7 +183,7 @@ let gen_of_delta resolve x kn fix_can =
   try
     let new_kn = solve_delta_kn resolve kn in
     if kn == new_kn then x else fix_can new_kn
-  with _ -> x
+  with e when Errors.noncritical e -> x
 
 let constant_of_delta resolve con =
   let kn = user_con con in
@@ -223,8 +224,10 @@ let constant_of_delta_with_inline resolve con =
   let kn1,kn2 = canonical_con con,user_con con in
   try find_inline_of_delta kn2 resolve
   with Not_found ->
-    try find_inline_of_delta kn1 resolve
-    with Not_found -> None
+    if kn1 == kn2 then None
+    else
+      try find_inline_of_delta kn1 resolve
+      with Not_found -> None
 
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
@@ -272,7 +275,9 @@ type sideconstantsubst =
   | Canonical
 
 let gen_subst_mp f sub mp1 mp2 =
-  match subst_mp0 sub mp1, subst_mp0 sub mp2 with
+  let o1 = subst_mp0 sub mp1 in
+  let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in
+  match o1, o2 with
     | None, None -> raise No_subst
     | Some (mp',resolve), None -> User, (f mp' mp2), resolve
     | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
diff --git a/kernel/modops.ml b/kernel/modops.ml
index af32288c..a81f868e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -33,7 +33,7 @@ type signature_mismatch_error =
   | NotConvertibleInductiveField of identifier
   | NotConvertibleConstructorField of identifier
   | NotConvertibleBodyField
-  | NotConvertibleTypeField
+  | NotConvertibleTypeField of env * types * types
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
diff --git a/kernel/modops.mli b/kernel/modops.mli
index d03d61bd..daea3258 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Univ
+open Term
 open Environ
 open Declarations
 open Entries
@@ -60,7 +61,7 @@ type signature_mismatch_error =
   | NotConvertibleInductiveField of identifier
   | NotConvertibleConstructorField of identifier
   | NotConvertibleBodyField
-  | NotConvertibleTypeField
+  | NotConvertibleTypeField of env * types * types
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
diff --git a/kernel/names.ml b/kernel/names.ml
index 17bda124..8c228404 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -205,7 +205,9 @@ type constant = kernel_name*kernel_name
 let constant_of_kn kn = (kn,kn)
 let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
 let make_con mp dir l = constant_of_kn (mp,dir,l)
-let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
+let make_con_equiv mp1 mp2 dir l =
+  if mp1 == mp2 then make_con mp1 dir l
+  else ((mp1,dir,l),(mp2,dir,l))
 let canonical_con con = snd con
 let user_con con = fst con
 let repr_con con = fst con
@@ -263,8 +265,10 @@ let constr_modpath c = ind_modpath (fst c)
 
 let mind_of_kn kn = (kn,kn)
 let mind_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_mind mp dir l = ((mp,dir,l),(mp,dir,l))
-let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
+let make_mind mp dir l = mind_of_kn (mp,dir,l)
+let make_mind_equiv mp1 mp2 dir l =
+  if mp1 == mp2 then make_mind mp1 dir l
+  else ((mp1,dir,l),(mp2,dir,l))
 let canonical_mind mind = snd mind
 let user_mind mind = fst mind
 let repr_mind mind = fst mind
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 6c08c34c..f0a3292c 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -90,7 +90,7 @@ let push_rel d env =
 
 let lookup_rel_val n env =
   try List.nth env.env_rel_val (n - 1)
-  with _ -> raise Not_found
+  with e when Errors.noncritical e -> raise Not_found
 
 let env_of_rel n env =
   { env with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1d606782..ec891e13 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -477,7 +477,7 @@ let end_module l restype senv =
    in
    let str = match sign with
      | SEBstruct(str_l) -> str_l
-     | _ -> error ("You cannot Include a high-order structure.")
+     | _ -> error ("You cannot Include a higher-order structure.")
    in
    let senv = update_resolver (add_delta_resolver resolver) senv
    in
@@ -873,7 +873,8 @@ end = struct
 	  let k = key_of_lazy_constr k in
 	  let access key =
 	    try (Lazy.force table).(key)
-	    with _ -> error "Error while retrieving an opaque body"
+	    with e when Errors.noncritical e ->
+              error "Error while retrieving an opaque body"
 	  in
 	  match load_proof with
 	    | Flags.Force ->
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index e2c5f48c..c809572a 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -219,6 +219,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
+    let err = NotConvertibleTypeField (env, t1, t2) in
+
     (* If the type of a constant is generated, it may mention
        non-variable algebraic universes that the general conversion
        algorithm is not ready to handle. Anyway, generated types of
@@ -257,12 +259,12 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
                  (the user has to use an explicit type in the interface *)
                 error NoTypeConstraintExpected
           with NotArity ->
-            error NotConvertibleTypeField end
+            error err end
         | _ ->
 	  t1,t2
       else
         (t1,t2) in
-    check_conv NotConvertibleTypeField cst conv_leq env t1 t2
+    check_conv err cst conv_leq env t1 t2
   in
 
   match info1 with
@@ -301,7 +303,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if constant_has_body cb2 then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
+      let error = NotConvertibleTypeField (env, arity1, typ2) in
+       check_conv error cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -312,7 +315,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if constant_has_body cb2 then error DefinitionFieldExpected;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv NotConvertibleTypeField cst conv env ty1 ty2
+      let error = NotConvertibleTypeField (env, ty1, ty2) in
+       check_conv error cst conv env ty1 ty2
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in