From bd0219b62a60cfc58c3c25858b41a005727c68be Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 13 Apr 2008 21:41:54 +0000 Subject: Bugs, nettoyage, et améliorations diverses - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/clenv.ml | 4 ++-- pretyping/clenv.mli | 4 +++- pretyping/evd.ml | 4 ++-- pretyping/pattern.ml | 2 +- pretyping/typing.ml | 2 +- 5 files changed, 9 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 242368ce99..e5632515d0 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -261,8 +261,8 @@ let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = * pose a value for it by constructing a fresh evar. We do this in * left-to-right order, so that every evar's type is always closed w.r.t. * metas. *) -let clenv_pose_dependent_evars clenv = - let dep_mvs = clenv_dependent false clenv in + +let clenv_pose_metas_as_evars clenv dep_mvs = List.fold_left (fun clenv mv -> let ty = clenv_meta_type clenv mv in diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 4f27ec902f..dfa7513495 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -79,7 +79,9 @@ val clenv_unique_resolver : val evar_clenv_unique_resolver : bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv -val clenv_pose_dependent_evars : clausenv -> clausenv +val clenv_dependent : bool -> clausenv -> metavariable list + +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv (***************************************************************) (* Bindings *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 2703e5ae0c..91b70e3b02 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -674,5 +674,5 @@ let pr_evar_defs evd = str"METAS:"++brk(0,1)++pr_meta_map evd.metas in v 0 (pp_evm ++ cstrs ++ pp_met) -let pr_metaset metas = - Metaset.fold (fun mv pp -> pr_meta mv ++ pp) metas (Pp.mt()) +let pr_metaset metas = + str "[" ++ prlist_with_sep spc pr_meta (Metaset.elements metas) ++ str "]" diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 90a3728ebb..05af1652e1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -92,7 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n - | Meta n -> PMeta (Some (id_of_string (string_of_int n))) + | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id | Sort (Prop c) -> PSort (RProp c) | Sort (Type _) -> PSort (RType None) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 32df490db8..ece3586a19 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -23,7 +23,7 @@ open Evd let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> error ("unknown meta ?"^string_of_int mv) in + with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in meta_instance evd ty let constant_type_knowing_parameters env cst jl = -- cgit v1.2.3