| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
pas correctes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- When the undo stack overflows, backtrack within a proof goes to
wrong state
- Boundary checks before undoing (popping the stack) wrong
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
receive their own name
as first argument. This is needed to make external tactics work when the external program
is interpreted and the operating system is Mac OS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10437 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
amélioration message d'erreur si nombre de pattern incorrect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
gratuit, je me suis décidé pour quelque chose de plus atomique).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
( ('a -> 'b -> bool) -> 'a option -> 'b option -> bool devient la même
chose mais avec 'a='b ) et de contenu pour avoir une sémantique plus
claire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10353 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un
ordinateur où j'ai pas installé lablgtk2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
parfaitement en cours) de la nouvelle machinerie de preuves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10251 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Unlike prlist_xxxx and prvect, the function prlist is acting lazily,
which is bad for extraction (synchronization with tables). We add and
use a prlist_strict function.
Additionaly:
- cleanup of the preamble printing
- no need for 2-pass printing (/dev/null trick) when the language
isn't ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10233 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
filtrage; sauts de line intempestifs dans pretty.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
the patch by S. Mimram)
* for detecting architecture, also look for /bin/uname
* restore the compatibility of kernel/byterun/coq_interp.c with
ocaml 3.07 (caml_modify vs. modify). There is still an issue
with this 3.07 and 64-bits architecture (see coqdev and a future
bug report).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
alias de variables dans la fonction d'inversion des instance (real_clean):
- détection des cas d'inversions distinctes incompatibles
- nouvelle heuristique lorsque plusieurs inversions distinctes mais
compatibles existent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10111 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
et Set Whelp Getter pour changer le nom des serveurs (report 10105 de
la 8.1 vers le trunk)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Documented in dev/doc/build-system.txt .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
utilities from Util. Some additions in Util, and simplifications
in various files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
When the system accepts a fixpoint, it now prints which decreasing argument
was used, e.g:
plus is recursively defined (decreasing on 1st argument)
The search is quite brute-force, and may need to be optimized for huge mutual
fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback.
N.B. in the standard library, only 4 functions have an decreasing argument
different from the one that would be automatically infered:
List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind
And compiling with as few explicit struct as possible would add about 15s
in compilation time for the whole standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
par sa notation (p.ex. pour unfold ou pour lazy delta).
Ex: Goal 3+4 = 7. unfold "+".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Club du 31/03/2007)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9741 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
compile-verbose +
ajout Pp.strbrk pour faciliter les césures faciles + messages divers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not
recompile the whole standard library just because the coq binaries
got rebuilt.
- Infrastructure to change the object pretty-printers at runtime.
- Use that infrastructure to make coqtop-protocol with Pcoq trees and
Pcoq-protocol with pretty-printed terms possible in coq-interface.
- Make "Back(track)" into closed sections, modules and module types
"Just Work™".
- Modernise/generalise Pcoq protocol a bit, make some of its warts
optional.
- Implement "Show." in Pcoq mode.
- Add Rpow_def.vo to REALSBASEVO so that its dependencies are
computed (and used).
- "make revision" now handles GNU Arch / tla in addition to svn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML
Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
xml-like patterns (<prompt></prompt>).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9191 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
castées si aussi suivies de leur type (p.ex. dans les hypothèses de but),
afin d'éviter des configurations non réinterprétables comme x:nat:nat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9164 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9151 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9130 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8867 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
between special characters.
I had to add a hidden variable print_emacs and a function to set it to
true in Pp because using Options.print_emacs would have introduce a
circularity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8748 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
between special characters.
I had to add a hidden variable print_emacs and a function to set it to
true in Pp because using Options.print_emacs would have introduce a
circularity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8747 85f007b7-540e-0410-9357-904b9bb8a0f7
|