diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 22:30:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 22:30:44 +0000 |
| commit | 7944955b892f0ffa70ecf92f83b372cddc5b867b (patch) | |
| tree | 479fc9f009fa1a81490c016956c61d6f7c62896c /pretyping | |
| parent | 90e5407fcfc59dce5ea592aeae6195183a2b4ad2 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index cb991ac9e..13ccefe1e 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 02f8e6fe8..bf72c9c7c 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 = |