| Age | Commit message (Collapse) | Author |
|---|
|
There are currently two other clashs : Lexer and Errors, but for
the moment these ones haven't impacted my experiments with extraction
and compiler-libs, while this Matching issue had. And anyway the new
name is more descriptive, in the spirit of the recent TacticMatching.
|
|
The comments were inaccurate after r16533.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in Tacinterp, and it allows to remove a lot of entangled exception
matchings in MatchGoal. Performance should not be affected, because
the structures manipulated are somehow similar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16533 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16531 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16483 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unnamed Metas; also added matching an applicative prefix (with
non-meta head) of a term against a pattern, to be used by "Search"
(i.e. SearchHead).
This allows "Search" and "SearchPattern" to behave as in 8.4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16422 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* in Matching and Tacinterp : ad-hoc types for encoding matching
result and "next" continuation
* in Class_tactics, occurrences of types such as
"type t = (foo * (unit->t) option"
have been specialized to something like
type t = TNone | TSome of foo * (unit -> t)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15869 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Instances found by matching.ml now collect the set of bound
variables they possibly depend on in the pattern (see type
Pattern.extended_patvar_map); the variables names are canonically
ordered so that non-linear matching takes actual names into account.
- Removed typing of matching constr instances in advance (in
tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback
is that we may have to re-type several times the same term but it is
necessary for considering terms with locally bound variables of which
we do not keep the type (and if even we had kept the type, we would have
to adjust the indices to the actual context the term occurs).
- A bit of documentation of pattern.mli, matching.mli and pretyping.mli.
- Incidentally add env while printing idtac messages. It seems more correct
and I hope I did not break some intended existing behavior.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
the naming of hypotheses (especially when doing "case H" with H of
type "{x|P<->Q}" since not unfolding will eventually introduce a name
"i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
of names manipulating type constr_pattern, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas
où c'est le n-ième sous-termes qui finalement réussit (passage à une
complexité en n plutôt que n^2, via l'utilisation de continuations).
- Sémantique du filtrage: suppression dans sub_match de la recherche
dans le type des let (puisque ce n'est pas cencé être une
information utilisateur) mais rajout de la recherche dans le champ
cast qui lui est utilisateur.
- Nouvelle fonctionnalité: récupération des noms des variables liantes
filtrées (dans matches/sub_match) et utilisation de ces noms dans
ltac (utile pour récupérer x dans "exists x, P x");
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
disambiguate syntax:
[ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x :
nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will
not parse.
Add applicative contexts in tactics match, to be able to match arbitrary partial
applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end
will bind C to [ ∙ 1 2 ] and x to 0.
Minor improvements in coqdoc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
sub_match qui est renommé par ailleurs en match_subterm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
|
