machine: execute = typage avec univers

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

1 files changed, 24 insertions, 24 deletions

diff --git a/kernel/evd.ml b/kernel/evd.ml
index 77351ab9b7..5b870d87af 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -12,11 +12,10 @@ type evar_body =
     EVAR_EMPTY | EVAR_DEFINED of constr
 
 type 'a evar_info = {
-  concl : constr;            (* the type of the evar ...          *)
-  hyps  : context;           (* ... under a certain signature     *)
-  body  : evar_body;         (* its definition                    *) 
-  info  : 'a option          (* any other necessary information   *)
-}         
+  evar_concl : typed_type;        (* the type of the evar ...          *)
+  evar_hyps  : context;           (* ... under a certain signature     *)
+  evar_body  : evar_body;         (* its definition                    *) 
+  evar_info  : 'a option }        (* any other necessary information   *)
 
 type 'a evar_map = 'a evar_info Spmap.t
 
@@ -34,31 +33,32 @@ let add_with_info evd sp newinfo =
 
 let add_noinfo evd sp sign typ = 
   let newinfo = 
-    { concl = typ;
-      hyps  = sign;
-      body  = EVAR_EMPTY;
-      info  = None}
+    { evar_concl = typ;
+      evar_hyps  = sign;
+      evar_body  = EVAR_EMPTY;
+      evar_info  = None}
   in 
   Spmap.add sp newinfo evd
 
 let define evd sp body = 
- let oldinfo = map evd sp in
- let newinfo =
-   { concl = oldinfo.concl;
-     hyps  = oldinfo.hyps;
-     body  = EVAR_DEFINED body;
-     info  = oldinfo.info} 
- in
- match oldinfo.body with
-   | EVAR_EMPTY -> Spmap.add sp newinfo evd
-   | _ -> anomaly "cannot define an isevar twice"
+  let oldinfo = map evd sp in
+  let newinfo =
+    { evar_concl = oldinfo.evar_concl;
+      evar_hyps  = oldinfo.evar_hyps;
+      evar_body  = EVAR_DEFINED body;
+      evar_info  = oldinfo.evar_info} 
+  in
+  match oldinfo.evar_body with
+    | EVAR_EMPTY -> Spmap.add sp newinfo evd
+    | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
 
 let non_instantiated sigma = 
-    let listsp = toList sigma in
-    List.fold_left 
-        (fun l ((sp,evd) as d) -> if evd.body = EVAR_EMPTY then (d::l) else l)
-        [] listsp
-
+  let listsp = toList sigma in
+  List.fold_left 
+    (fun l ((sp,evd) as d) -> 
+       if evd.evar_body = EVAR_EMPTY then (d::l) else l)
+    [] listsp
+    
 let is_evar sigma sp = in_dom sigma sp