| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
for adding spaces were not taken into account in notations containing
patterns of the form "{ ident symbol", paradoxically resulting in
adding extra spaces, e.g. when printing the type "{ x | P x }" of
"exist", due to interferences with the heuristic for adding breaking
points in Metasyntax.make_hunk).
Also adapted output of test InitSyntax.v after commit r14018 improved
the printing of "ex P" and "sig P".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Missing space and bad constr level in "About f"
- Display of arguments missing when used as a pattern notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13946 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Probably something related with the unicode lambda syntax...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13911 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13910 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
In particular, the Fail meta-command cannot for the moment catch a Syntax Error,
which is raised by Vernac.parse_sentence, before we even now that the line starts
by a Fail...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
The new output makes sense with the new "1 subgoal = 1 evar" paradigm
introduced with by the new proof engine.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13487 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".
This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- use list of non-newline-ended phrases instead of newline-separated
texts because newline-separated texts does not support well being
put in boxes (e.g. ''v 2 (str"a" ++ fnl()) ++ str"b" ++ fnl()''
prints "b" at indentation 2 while to get the expected output, one
would have needed to have the fnl outside the box as in
''v 2 (str"a") ++ fnl() ++ str"b" ++ fnl()''
- also reason over lists of explicitly non-empty lines instead of
checking for "mt" lines to skip
The reason of this is to permit nesting of printing infos.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13482 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation
Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Note that the code is no longer in constrextern.ml but in topconstr.ml where
the code for reversing notations of term already was.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
match predicate) and fixed Notation.out test accordingly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- Notations with coercions to funclass inserted were not working any
longer since r11886. Made a fix but maybe should we eventually type
the notations so that they have a canonical form (and in particular
with coercions pre-inserted?).
- Improved spacing management in printing extra tactic arguments "by" and "in".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
numerals are open (see e.g. part of bug report #2044).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12924 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12860 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Having to alias the inductive BigN.t_ by a constant BigN.t
for satisfying the NSig interface is just a pain. Let's hope
it could change someday.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12703 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Removed one more bug in simplification of visibly_occur_id in r12549
+ improved CHANGES message
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- fixed misunderstanding of the role of nenv while simplifying code of
occur_id in namegen.ml,
- documented the possible incompatibilites in CHANGES
- fixed output/Naming.v test, and fixed the count of misc. tests in
test-suite/check.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- backtrack on incompatibility introduced in intro while trying to
simplify the condition about when to restart the subscript of a name
(the legacy says: find a new name from x0 if the name xN exists in
the context but find a new name from xN+1 if the name xN does not
exists in the context but is a global to avoid).
- made the names chosen by "intro" compliant with the ones printed in
the goal and used for "intros until" (possible source of rare
incompatibilities) [replaced the use of visibly_occur_id for
printing the goal into a call to next_name_away_in_goal]
- also made the names internal to T in "T -> U" printed the same in
the goal as they are while printing T after it is introducted in the
hypotheses [non contravariant propagation of boolean isgoal in
detype_binder]
- simplified a bit visibly_occur_id (the Rel and Var cases were useless as
soon as the avoid list contained the current env); still this function is
costly with polynomial time in the depth of binders
- see file output/Naming.v for examples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- In fact, Bind Scope has no retrospective effect. Since we don't want
it inside functor, we use it late, and hence we are forced to use manual
"Arguments Scope" commands.
- Added syntax for power in BigN / BigZ / BigQ.
- Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq)
as in QArith. Display of a rational numeral is hence either an integer
(constructor BigQ.Qz) or something like 6756 # 8798.
- Fix of function BigQ.Qred that was not simplifing (67#1) into 67.
- More tests in test-suite/output/NumbersSyntax.v
A nice one not in the test-suite:
Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)).
= 1
: bigQ
Finished transaction in 3. secs (3.284206u,0.004s)
:-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12507 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
on the way:
- Added a testsuite output file
- Try to avoid nasty unfolding (fix nfun ...) in type of I31.
Idealy we would need a "Eval compute in" for the type of a inductive
constructor
- Stop opening Scopes for BigQ, BigN, BigZ by default
The user should do some Open Scope.
TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope
(and so on for other operations), even with some Bind Scope around.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- Adding test file related to commit 12080 (bug #2091).
- Cleaning old parsing stuff from 8.0.
- Support for camlp5 in base_include.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12096 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12038 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
coercion to funclass) [added a new notation output test as the
initial one is quite saturated in miscellaneous notations].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
late 2008 Coq WG.
- Updated Copyright file wrt JProver.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11740 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11736 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Fixed a virtual bug of unification (ever occurs if w_unify called with
a non-empty context of rel's, which is a priori uncommon).
- Fixed Notation.out test.
- Add better coqide error message in case editor is called on an unnamed file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Ajout test pour non-régression du bug #1968
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- Correction bug #1815 sur "coqide dir_inexistant/nom_fichier"
- Tests oubliés de la révision 11438 (amélioration affichage coercions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
entre le calcul des arguments récursifs possibles -- bien que bidon en
attendant mieux -- et ce la tactique fix attend -- le premier expanse
les produits au maximum le second non)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives
sous forme de terme par une représentation directe (permet notamment
de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7
|