diff options
author | 2007-05-20 17:44:23 +0000 | |
---|---|---|
committer | 2007-05-20 17:44:23 +0000 | |
commit | 9accb5a66da5d68fa01c4c3b8e7b74985e84f6fa (patch) | |
tree | 59ccd22002952d3557ee0cb8f0299c232813f2a7 /proofs/tacexpr.ml | |
parent | 08f7d8d83fd0a5f18ae764a21a21b5336a0ce7f5 (diff) |
- 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
Diffstat (limited to 'proofs/tacexpr.ml')
-rw-r--r-- | proofs/tacexpr.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b06ec2f49..c78e842ec 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 |