A try at using sort variables during unification. Instead of refreshing

universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort 
constraints are thrown away at the end of unification for the moment, 
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.


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

1 files changed, 10 insertions, 10 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e7682285b9..8e9ddf1baf 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -947,22 +947,22 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_evars evd t =
-  let evm =  evd in
+let has_undefined_evars_or_sorts evd t =
   let rec has_ev t =
     match kind_of_term t with
-        Evar (ev,args) ->
-          (match evar_body (Evd.find evm ev) with
-            | Evar_defined c ->
-                has_ev c; Array.iter has_ev args
-            | Evar_empty ->
-	        raise NotInstantiatedEvar)
-      | _ -> iter_constr has_ev t in
+    | Evar (ev,args) ->
+        (match evar_body (Evd.find evd ev) with
+        | Evar_defined c ->
+            has_ev c; Array.iter has_ev args
+        | Evar_empty ->
+	    raise NotInstantiatedEvar)
+    | Sort s when is_sort_variable evd s -> raise Not_found
+    | _ -> iter_constr has_ev t in
   try let _ = has_ev t in false
   with (Not_found | NotInstantiatedEvar) -> true
 
 let is_ground_term evd t =
-  not (has_undefined_evars evd t)
+  not (has_undefined_evars_or_sorts evd t)
 
 let is_ground_env evd env =
   let is_ground_decl = function