aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
AgeCommit message (Collapse)Author
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
2004-01-26a try to make intro patterns betterbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5247 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-24streamlines the keywords for definitions, require commandsbinders, notationbertot
definitions, Show commands, Print commands, proof starting commands, Search commands, scope commands, type reservation command, locate commands, time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5244 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22change add path commands to get the extra argument and the Hint commandsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5239 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22fixes argument lists for tactic definitions, updates inversion tacticsbertot
so that they use intro-pattern-lists like induction and destruct git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5236 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22adds a clause argument to symmetrybertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5235 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22corrects the way the structural argument declaration is handled inbertot
fixpoint definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5234 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22adds the notations in inductive definitions, improves the consistency betweenbertot
induction et destruct, takes the extra argument for fail and idtac into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5233 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22handles explicit function calls, names meta variables in patternsbertot
(in V8 the name is not a number), explicitation of arguments with names (but not with rank anymore), the refine tactic now has its own operator the structure information for hypotheses in induction is now handled as in intro, the tactic instantiate has been modified to use clauses, the wildcard rule for Ltac pattern matching on goals has been added and the possibility to refer to types of values and instantiated contexts in values in Ltac have been added. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5232 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-21updates the structure of fix (struct argument added) and ifbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5225 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-19handles projector notations, cases with return types,bertot
tuple lets, and a few tactics whose name appears with an upper case initial git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5218 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-191.20bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5217 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-191.19bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5216 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-19adds constructs to handle notations in patternsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5215 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15translation to structures now okay for pattern matching constructsbertot
The locations in simpl, unfold, and the like are also better taken into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5209 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14compact nested universal quantifications into a single quantification withbertot
a list of binders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5204 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 02:40:37 +0000