diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 19:11:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 19:11:52 +0000 |
| commit | 14d08596263d9247b7a32bc6528f0a649e6f7908 (patch) | |
| tree | 02ba3c281bc095d5fad380e64a6e201ed6c03d27 /tactics/dhyp.ml | |
| parent | ad6d5fe6353ec5faf0a39f844fa58673cf50cff0 (diff) | |
Déplacement du type reference dans Term
Découpage de tactics/pattern en proofs/pattern et tactics/hipattern
Renommage des fonctions somatch and co dans Pattern et Tacticals
Divers extensions pour utiliser les constr_pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/dhyp.ml')
| -rw-r--r-- | tactics/dhyp.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 0ca3f6b2a..a21b3e6d7 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -128,8 +128,8 @@ open Pcoq (* two patterns - one for the type, and one for the type of the type *) type destructor_pattern = { - d_typ: Rawterm.constr_pattern; - d_sort: Rawterm.constr_pattern } + d_typ: constr_pattern; + d_sort: constr_pattern } type ('a,'b) location = Hyp of 'a | Concl of 'b @@ -222,11 +222,11 @@ let _ = add_destructor_hint na (match loc with | Hyp b -> - Hyp(b,{d_typ=pat;d_sort=PMeta(new_meta())}, - { d_typ=PMeta(new_meta()); - d_sort=PMeta(new_meta()) }) + Hyp(b,{d_typ=pat;d_sort=PMeta(Some (new_meta()))}, + { d_typ=PMeta(Some (new_meta())); + d_sort=PMeta(Some (new_meta())) }) | Concl () -> - Concl({d_typ=pat;d_sort=PMeta(new_meta())})) + Concl({d_typ=pat;d_sort=PMeta(Some (new_meta()))})) pri code | _ -> bad_vernac_args "HintDestruct") @@ -234,13 +234,13 @@ let match_dpat dp cls gls = let cltyp = clause_type cls gls in match (cls,dp) with | (Some id,Hyp(_,hypd,concld)) -> - (somatch None hypd.d_typ cltyp)@ - (somatch None hypd.d_sort (pf_type_of gls cltyp))@ - (somatch None concld.d_typ (pf_concl gls))@ - (somatch None concld.d_sort (pf_type_of gls (pf_concl gls))) + (matches hypd.d_typ cltyp)@ + (matches hypd.d_sort (pf_type_of gls cltyp))@ + (matches concld.d_typ (pf_concl gls))@ + (matches concld.d_sort (pf_type_of gls (pf_concl gls))) | (None,Concl concld) -> - (somatch None concld.d_typ (pf_concl gls))@ - (somatch None concld.d_sort (pf_type_of gls (pf_concl gls))) + (matches concld.d_typ (pf_concl gls))@ + (matches concld.d_sort (pf_type_of gls (pf_concl gls))) | _ -> error "ApplyDestructor" let applyDestructor cls discard dd gls = |