Modifications diverses et variées :

- Nouvel essai de prise en compte unfold dans apply (unification.ml)
- Correction bug commit précédent (constrintern.ml)
- Correction bug d'explication des evars non résolues (evarutil.ml)
- Fenêtre de query coqide plus large (command_windows.ml)
- Orthographe tauto (tauto.ml4)
- Crédits (ConstructiveEpsilon.v)



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

6 files changed, 10 insertions, 6 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 5887492ce6..b933b7ce2c 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -11,7 +11,7 @@
 class command_window () = 
   let window = GWindow.window 
 		 ~allow_grow:true ~allow_shrink:true 
-		 ~width:320 ~height:200
+		 ~width:500 ~height:250
 		 ~position:`CENTER
 		 ~title:"CoqIde queries" ~show:false ()
   in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a0e9b6bb5f..55f3d9fba2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -606,7 +606,7 @@ let find_constructor ref f aliases pats scopes =
 	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
 	   let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in
 	   cstr, idspl1, pats2
-       | _ -> error_invalid_pattern_notation loc)
+       | _ -> raise Not_found)
       
   | TrueGlobal r ->
       let rec unf = function
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cb991ac9e5..13ccefe1e4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1074,7 +1074,9 @@ let check_evars env initial_sigma evd c =
             let (loc,k) = evar_source evk evd in
 	    let evi = nf_evar_info sigma (Evd.find sigma evk) in
 	    let explain =
-	      let f (_,_,t1,t2) = head_evar t1 = evk or head_evar t2 = evk in
+	      let f (_,_,t1,t2) =
+		(try head_evar t1 = evk with Failure _ -> false)
+		or (try head_evar t2 = evk with Failure _ -> false) in
 	      let check_several c inst =
 		let _,argsv = destEvar c in
 		let l = List.filter (eq_constr inst) (Array.to_list argsv) in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 02f8e6fe8e..bf72c9c7c5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -132,7 +132,7 @@ type unify_flags = {
 let default_unify_flags = {
   modulo_conv_on_closed_terms = true;
   use_metas_eagerly = true;
-  modulo_delta = Cpred.empty;
+  modulo_delta = Cpred.full;
 }
 
 let unify_0_with_initial_metas metas is_subterm env sigma cv_pb flags m n =
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 3c65fe1592..0207f1fb93 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -23,7 +23,7 @@ open Util
 let assoc_last ist =
   match List.assoc (Names.id_of_string "X1") ist.lfun with
     | VConstr c -> c
-    | _ -> failwith "Tauto: anomaly"
+    | _ -> failwith "tauto: anomaly"
 
 let is_empty ist =
   if is_empty_type (assoc_last ist) then
@@ -165,7 +165,7 @@ let tauto g =
   try intuition_gen (interp <:tactic<fail>>) g
   with
     Refiner.FailError _ | UserError _ ->
-      errorlabstrm "tauto" [< str "Tauto failed" >]
+      errorlabstrm "tauto" [< str "tauto failed" >]
 
 let default_intuition_tac = interp <:tactic< auto with * >>
 
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 322f2d9be9..fe571779ca 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -31,6 +31,8 @@ To use [Fix_F], we define a relation R and prove that if [exists n,
 P n] then 0 is accessible with respect to R. Then, by induction on the
 definition of [Acc R 0], we show [{n : nat | P n}]. *)
 
+(** Based on ideas from Benjamin Werner and Jean-François Monin *)
+
 (** Contributed by Yevgeniy Makarov *)
 
 Require Import Arith.