gros commit de tout ce que j'ai fait pendant les vacances :

 - tactics/Equality
 - debug du discharge
 - constr_of_compattern implante vite fait / mal fait en attendant mieux
 - theories/Logic (ne passe pas entierrement)


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

4 files changed, 23 insertions, 23 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 34cf69ac2a..b114e1b542 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -75,8 +75,8 @@ let inh_app_fun env isevars j =
 (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *)
 
 let inh_tosort_force env isevars j =
-  let t,i1 = class_of1 env !isevars j.uj_type in
   try
+    let t,i1 = class_of1 env !isevars j.uj_type in
     let p = lookup_path_to_sort_from i1 in
     apply_pcoercion env p j t 
   with Not_found -> 
@@ -85,20 +85,17 @@ let inh_tosort_force env isevars j =
 let inh_tosort env isevars j = 
   let typ = whd_betadeltaiota env !isevars j.uj_type in
   match typ with
-    | DOP0(Sort(_)) -> j  (* idem inh_app_fun *)
+    | DOP0(Sort _) -> j  (* idem inh_app_fun *)
     | _ -> (try inh_tosort_force env isevars j with _ -> j)
 
 let inh_ass_of_j env isevars j =
   let typ = whd_betadeltaiota env !isevars j.uj_type in
   match typ with
-    | DOP0(Sort s) -> {body=j.uj_val;typ=s}
+    | DOP0(Sort s) -> 
+	{ body = j.uj_val; typ = s }
     | _ ->
-        (try
-           let j1 = inh_tosort_force env isevars j in 
-	   assumption_of_judgment env !isevars j1 
-         with _ -> 
-	   error_assumption CCI env (nf_ise1 !isevars j.uj_val))
-           (* try ... with _ -> ... is BAD *)
+        let j1 = inh_tosort_force env isevars j in 
+	assumption_of_judgment env !isevars j1 
 
 let inh_coerce_to1 env isevars c1 v t k =
   let t1,i1 = class_of1 env !isevars c1 in
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index c510299acf..1c80cdb9f2 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -17,12 +17,13 @@ val inh_tosort_force :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_tosort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-val inh_ass_of_j : env -> 'a evar_defs ->
-  unsafe_judgment -> typed_type
-val inh_coerce_to : env -> 'a evar_defs ->
-  constr -> unsafe_judgment -> unsafe_judgment
-val inh_cast_rel : env -> 'a evar_defs ->
-  unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+val inh_ass_of_j : 
+  env -> 'a evar_defs -> unsafe_judgment -> typed_type
+val inh_coerce_to : 
+  env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment
+val inh_cast_rel : 
+  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+
 val inh_apply_rel_list : bool -> env -> 'a evar_defs ->
   unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) 
     -> unsafe_judgment
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 53bcbc8ce5..2f07574127 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -77,11 +77,11 @@ let split_evar_to_arrow sigma c =
   let prod = prod_create nevenv (incast_type dom, 
 				 subst_var nvar (body_of_type rng)) in
   let sigma3 = Evd.define sigma2 ev prod in
-  let dsp = path_of_const (body_of_type dom) in
-  let rsp = path_of_const (body_of_type rng) in
+  let dsp = num_of_evar (body_of_type dom) in
+  let rsp = num_of_evar (body_of_type rng) in
   (sigma3,
-   mkCast (mkConst (dsp,args)) dummy_sort,
-   mkCast (mkConst (rsp,array_cons (mkRel 1) args)) dummy_sort)
+   mkCast (mkEvar dsp args) dummy_sort,
+   mkCast (mkEvar rsp (array_cons (mkRel 1) args)) dummy_sort)
 
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -193,7 +193,7 @@ let real_clean isevars sp args rhs =
     | DLAM(n,a) -> DLAM(n, subs (k+1) a)
     | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v) in
   let body = subs 0 rhs in
-  if not (closed0 body) then error_not_clean CCI empty_env sp body;
+  (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
   body
 
 
@@ -303,7 +303,7 @@ let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) =
   else 
     match (ise_undefined isevars t1, ise_undefined isevars t2) with
       | (true,true) ->
-	  if path_of_const t1 = path_of_const t2 then 
+	  if num_of_evar t1 = num_of_evar t2 then 
 	    solve_refl conv_algo isevars t1 t2
 	  else if Array.length(args_of_const t1) < 
 	          Array.length(args_of_const t2) then 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1854e7eebd..4ce29088da 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -509,8 +509,10 @@ let ise_resolve_nocheck sigma metamap env c =
 
 
 let ise_resolve1 is_ass sigma env c =
-  if is_ass then body_of_type (ise_resolve_type true sigma [] env c)
-  else (ise_resolve true sigma [] env c).uj_val
+  if is_ass then 
+    body_of_type (ise_resolve_type true sigma [] env c)
+  else 
+    (ise_resolve true sigma [] env c).uj_val
 
 (* Keeping universe constraints *)
 (*