aboutsummaryrefslogtreecommitdiff
path: root/toplevel/command.mli
AgeCommit message (Collapse)Author
2009-11-27Added support for definition of fixpoints using tactics.herbelin
Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
- Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
by Context. Now Context has exactly the same semantics as Variables. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
definitions and variables (may increase the vo's size a bit), which in turn fixes discharging with manual implicit args only. Fix Context to correctly handle "kept" assumptions for typeclasses, discharging a class variable when any variable bound in it is used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12150 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-13 Fix to my last notation patch: now fixpoint are correctly handled vsiles
when it comes to notation declared in scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12125 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
by user) and #2017 (unification pattern test too crude leading to regression wrt to 8.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11743 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
CoInductive stream (A:Type) := { hd : A ; tl : stream A }. Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }. L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de la syntaxe qui était apparue dans la 8.2beta pour les records coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" comme maintenant). VernacRecord et VernacInductive semblent maintenant faire doublon, il doit y avoir moyen de les fusionner. Les records mutuellement inductifs restent aussi à faire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Fix bug #1913, checking for unresolved evars which aren't obligations.msozeau
Also check mutuality of fixpoints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11257 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
types. Change (again) the semantics of bindings and the binding modifier ! in typeclasses. Inside [ ], implicit binding where only parameters need to be given is the default, use ! to use explicit binding, which is equivalent to regular bindings except for generalization of free variables. Outside brackets (e.g. on the right of instance declarations), explicit binding is the default, and implicit binding can be used by adding ! in front. This avoids almost every use of ! in the standard library and in other examples I have. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-15Do a second pass on the treatment of user-given implicit arguments. Nowmsozeau
works in inductive type definitions and fixpoints. The semantics of an implicit inductive parameter is maybe a bit weird: it is implicit in the inductive definition of constructors and the contructor types but not in the inductive type itself (ie. to model the fact that one rarely wants A in vector A n to be implicit but in vnil yes). Example in test-suite/ Also, correct the handling of the implicit arguments across sections. Every definition which had no explicitely given implicit arguments was treated as if we asked to do global automatic implicit arguments on section closing. Hence some arguments were given implicit status for no apparent reason. Also correct and test the parsing rule which disambiguates between {wf ..} and {A ..}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10677 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
(Axiom/Variable...). New tactic clapply to apply unapplied class methods in tactic mode, simple solution to the fact that apply does not work up-to classes yet. Add Functions.v for class definitions related to functional morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-22Merge with lmamane's private branch:lmamane
- 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
2008-02-10Backport Program Instance into Instance. Proper early error message ifmsozeau
trying to declare an instance with an already existing name. Add possibility of not giving all the fields in Instance declarations, using Refine.refine to generate the subgoals. No control over opacity in this case though... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
recursive definitions. Now program accepts cofixpoints and uses the new way infer structurally decreasing arguments. Also, checks for correct recursive calls before giving the definition to the obligations machine (solves part 1 of bug #1784). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
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
2007-09-28Modification of the Scheme command.vsiles
Now you can forget to provide the name of the scheme, it will be built automatically depending of the sorts involved. e.g. Scheme Induction for nat Sort Set. will build nat_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-28Support for implicit formal argument types in Program ; parse types in type ↵msozeau
scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9734 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an ↵msozeau
obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-23Addition of a "Combined Scheme" vernacular command for building the ↵msozeau
conjunction of mutual inductions principles. e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
(+ uniformisation position notation dans les blocs inductifs et récursifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵herbelin
dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31Export de l'information si un inductive est un record ou non (pour xml)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5622 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id ↵herbelin
:= c" de "Notation "'id'" := c" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵herbelin
a b:A' et 'Variables (a:A) (b:A)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-02meilleure presentation des commentaires du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵herbelin
incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Mise en place structure pour des 'arguments scope' dirigés par une classeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4118 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ↵herbelin
points-fixes; prise en compte par le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourherbelin
les définitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et ↵herbelin
retouche des Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:26:34 +0000