- Fix uncaught exception NotASort from reductionops, moving decomp_sort to retyping.ml

- In unification's w_merge, assign the evars in the same order they were found. Might
create rare incompatibilities.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16632 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 12 insertions, 13 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b2a9bdcc5..e86732658 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -939,16 +939,10 @@ let splay_lam_n env sigma n =
   in
   decrec env n empty_rel_context
 
-exception NotASort
-
-let decomp_sort env sigma t =
+let is_sort env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-  | Sort s -> s
-  | _ -> raise NotASort
-
-let is_sort env sigma arity =
-  try let _ = decomp_sort env sigma arity in true
-  with NotASort -> false
+  | Sort s -> true
+  | _ -> false
 
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e95fc41c0..588914c58 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -181,8 +181,6 @@ val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_prod_assum :
   env ->  evar_map -> constr -> rel_context * constr
-val decomp_sort : env -> evar_map -> types -> sorts
-val is_sort : env -> evar_map -> types -> bool
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
@@ -196,6 +194,7 @@ val reduce_mind_case : constr miota_args -> constr
 
 val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term
 val is_arity : env ->  evar_map -> constr -> bool
+val is_sort : env -> evar_map -> types -> bool
 
 val whd_programs :  reduction_function
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index c61872091..f5f977615 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -76,6 +76,11 @@ let sort_of_atomic_type env sigma ft args =
     | _ -> retype_error NotASort
   in concl_of_arity env ft (Array.to_list args)
 
+let decomp_sort env sigma t =
+  match kind_of_term (whd_betadeltaiota env sigma t) with
+  | Sort s -> s
+  | _ -> retype_error NotASort
+
 let type_of_var env id =
   try let (_,_,ty) = lookup_named id env in ty
   with Not_found -> retype_error (BadVariable id)
@@ -165,7 +170,8 @@ let retype ?(polyprop=true) sigma =
     | App(f,args) ->
 	family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
-    | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
+    | _ -> 
+      family_of_sort (decomp_sort env sigma (type_of env t))
 
   and type_of_global_reference_knowing_parameters env c args =
     let argtyps =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5dd794243..14d6ad333 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -950,7 +950,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in
 
   (* merge constraints *)
-  w_merge_rec evd (order_metas metas) evars []
+  w_merge_rec evd (order_metas metas) (List.rev evars) []
 
 let w_unify_meta_types env ?(flags=default_unify_flags) evd =
   let metas,evd = retract_coercible_metas evd in