aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
AgeCommit message (Collapse)Author
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵herbelin
tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Correction 1.138 appliquée à tort à la branche principale au lieu de ↵herbelin
V8-0bugfix; retour version 1.137 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6379 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Commit précédent erroné; retour version précédenteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6377 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28MAJ vis à vis de extratacticsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6368 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Locate Moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6325 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 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-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵herbelin
evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Show Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5967 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-18Abstraction vis a vis du type loc pour ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5951 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-06-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29License de contrib/interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5849 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28contrib/interface *$*$@!corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5844 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21pb install de pcoqbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5695 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation pour release (suite)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5497 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15To make that the translation process does not fail on data produced bybertot
the logical engine (rather than the parser), where Some Anonymous appears instead of None in the patterns of xlate_return_info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5486 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03takes better account of the new possibility to pass a parametric count argumentbertot
to both 'do' and 'fail' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5425 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03removes capital letters in two tactic names.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5424 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03make sure the implicit argument indications are in the right orderbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5423 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵herbelin
noms d'hypothèses; Changement de natural en int_or_var pour 'do' et 'fail' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5420 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵herbelin
variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Ajout IntroPattern comme type d'argument génériqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5407 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Not all cases for coercions and locality were handledbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5385 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-23corrects the treatement of SubClass declarationsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5372 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-19makes sure the following examples are well-treated:bertot
Export X. conditional trivial rewrite nat_le_correct in H. firstorder. Definition error := @None. Proof with trivial. Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l with minus := Rminus div := Rdiv. Ltac ElimPcompare c1 c2 := let x := fresh H in intro x. simplify_eq H. Extraction Inline list_length_induction. Extraction NoInline code insert isort map frequency_list huffman encode decode. ajoute une modification dans le traitement de let_tuple git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5363 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16accomodate the .. extensionbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5350 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16adds a new command for searching a pattern inside the premises of theoremsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5349 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16corrects a bug in name reservation, simplifies or_intro, removes dead codebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5348 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13adds a new command add_rec_path for the parser program and changes add_pathbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5337 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13adds the possibility to have terms (and not just identifiers) as hintsbertot
Adds the 'Reserved Notation' command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5335 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13adds the possibility to have terms (and not just identifiers) as hintsbertot
Adds the 'Reserved Notation' command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5334 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12lazy was translated to cbv, obviously wrongbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5322 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Implicits can have an optional list of argument, which is differentbertot
from an empty list of arguments. in H at 2 |- * was badly translated in clauses (for replacement tactics) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5318 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-11a new version that uses intro patterns, but the code still needs some cleaningbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5316 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-11removes a lot comments that may be useful for later code maintenance, butbertot
should not be kept in the sources because they only contain obsolete code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5315 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
uncapitalizes dependentrewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5277 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5276 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30updates the definition of tactics using Ltac and adds the subst tacticbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5274 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30adds module commands and update the extration commandbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5273 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-29updates the tactics contradiction and autorewrite, the commandsbertot
set implicit arguments, hint rewrite, and proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5263 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28make sure that 'in' clauses for reduction tactics are translatedbertot
once again re-organize the way intro patterns are translated: there is now only one kind of pattern that can be used for both and and or constructs: the use of the multiplet notation should only be a matter of notation. un-capitalize a few tactic names for tactics represented using the TacExtend construct. corrects a bug in the way binders or coercion binders were used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5260 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-17 06:48:05 +0000