From e653b53692e2cc0bb4f84881b32d3242ea39be86 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Thu, 19 Feb 2009 19:13:50 +0000 Subject: On remplace evar_map par evar_defs (seul evar_defs est désormais exporté par Evd). Ça s'accompagne de quelques autres modifications de l'interface (certaines fonctions étaient des doublons, ou des conversions entre evar_map et evar_defs). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit J'ai modifié un peu la structure de evd.ml aussi, pour éviter des fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai introduit des sous-modules pour les différentes couches. Il y a à l'heure actuelle une pénalité en performance assez sévère (due principalement à la nouvelle mouture de Evd.merge, si mon diagnostique est correct). Mais fera l'objet de plusieurs optimisations dans les commits à venir. Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un appel de Decl_proof_instr.mark_as_done visiblement, je suis pour l'instant incapable de comprendre ce qui cause cette erreur. J'espère qu'on pourra le déterminer rapidement. Ce commit est le tout premier commit dans le trunk en rapport avec les évolution futures de la machine de preuve, en vue en particulier d'obtenir un "vrai refine". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/typeclasses_errors.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typeclasses_errors.ml') diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index ba3eae6fa..fc4362875 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev = | None -> raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) | Some ev -> - let evi = Evd.find (Evd.evars_of evd) ev in + let evi = Evd.find ( evd) ev in let loc, kind = Evd.evar_source ev evd in raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (evi, kind))))) -- cgit v1.2.3