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

1 files changed, 1 insertions, 1 deletions

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 =