diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 16:25:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 16:25:05 +0000 |
| commit | bc8728f0762f7e39f779c677679a8bc351a4290a (patch) | |
| tree | b8a131508fcd4bc0ca131d4032788316b08b6997 /parsing/q_coqast.ml4 | |
| parent | 2814afbbd4803216ad4cb6af9ec5d86fce71e8eb (diff) | |
- Relâchement de la contrainte de bonne longueur des intropatterns
lorsqu'en position terminale (en fait, l'idéal serait de pouvoir
mettre des tactiques dans les branches, style "intros [H ; tac | ]")
(cf un exemple QvMake.v)
- Pas de delta du tout quand on fait de la recherche de sous-terme
(même lorsqu'on vient de apply avec une conclusion ?P t) (cf un
exemple dans Rocq/DEMOS/Sorting.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 55b531585..d961dc2f2 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -67,12 +67,13 @@ let mlexpr_of_by_notation f = function | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> let mlexpr_of_intro_pattern = function - | Genarg.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >> | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >> | Genarg.IntroIdentifier id -> <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ -> + failwith "mlexpr_of_intro_pattern: TODO" let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) |