From 9accb5a66da5d68fa01c4c3b8e7b74985e84f6fa Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 20 May 2007 17:44:23 +0000 Subject: - Propagation des evars non résolues vers les with_bindings; permet par exemple de résoudre des buts comme celui-ci : Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenvtac.ml | 4 ++-- proofs/proof_type.ml | 6 +++--- proofs/proof_type.mli | 6 +++--- proofs/refiner.mli | 2 +- proofs/tacexpr.ml | 8 ++------ 5 files changed, 11 insertions(+), 15 deletions(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8bba760074..db94fad149 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -49,7 +49,7 @@ let clenv_cast_meta clenv = match kind_of_term (strip_outer_cast u) with | Meta mv -> (try - let b = Typing.meta_type clenv.env mv in + let b = Typing.meta_type clenv.evd mv in if occur_meta b then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) @@ -62,7 +62,7 @@ let clenv_cast_meta clenv = let clenv_refine clenv gls = tclTHEN - (tclEVARS (evars_of clenv.env)) + (tclEVARS (evars_of clenv.evd)) (refine (clenv_cast_meta clenv (clenv_value clenv))) gls diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 20ce39775c..dfe0ab76d4 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -73,7 +73,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -83,7 +83,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index f835e2ef42..c06aff7e14 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -108,7 +108,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -118,7 +118,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 43d5af159d..03a32bab87 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val abstract_operation : compound_rule -> tactic -> tactic val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic val abstract_extended_tactic : - ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic + ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic val refiner : rule -> tactic val frontier : transformation_tactic diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b06ec2f496..c78e842ec0 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -306,16 +306,12 @@ type glob_generic_argument = rawconstr_and_expr generic_argument type glob_red_expr = (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen -type closed_raw_generic_argument = constr_expr generic_argument +type typed_generic_argument = Evd.open_constr generic_argument type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type -type open_generic_argument = Term.constr generic_argument - -type closed_generic_argument = Term.constr generic_argument - -type 'a closed_abstract_argument_type = ('a,Term.constr) abstract_argument_type +type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type type declaration_hook = Decl_kinds.strength -> global_reference -> unit -- cgit v1.2.3