diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /proofs/proof_type.ml | |
| parent | 77259e0b563a10d57b55ac38400ca1843fb938f3 (diff) | |
Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index bf8deb53a..363dd0964 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -28,6 +28,10 @@ type pf_status = | Complete_proof | Incomplete_proof +type hyp_location = (* To distinguish body and type of local defs *) + | InHyp of identifier + | InHypType of identifier + type prim_rule_name = | Intro | Intro_after @@ -37,6 +41,8 @@ type prim_rule_name = | Refine | Convert_concl | Convert_hyp + | Convert_defbody + | Convert_deftype | Thin | Move of bool @@ -97,7 +103,7 @@ and tactic_arg = | Identifier of identifier | Qualid of Nametab.qualid | Integer of int - | Clause of identifier list + | Clause of hyp_location list | Bindings of Coqast.t substitution | Cbindings of constr substitution | Quoted_string of string |