aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
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-15oopscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5485 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14minor changescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5480 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14congruence now handles disequalitiescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5479 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-13Mise en place temporaire d'un afficheur de 'language' pour le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5474 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ooops ! bug in firstorder fixed (let's hope no one noticed)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5456 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11reals: renamed type option into field_rel_optionmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5451 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-04Reparation ROmega V8/Omega ZERO/POS/NEGmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5431 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03adaptation V8 version Pierre Cregutmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5428 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-01code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5410 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-03-01Protection d'un 'clear' qui peut etre dependantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5403 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-13petit bug avec Extraction Optimizeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5339 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-10Correction of a bug in Functional Scheme discovered when porting thecoq
contrib QArith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5313 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
more functions (higher order and polymorphic functions), the principle is a bit better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5310 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-06correction de bugs de congruence et firstorder (inductifs)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5303 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:59:03 +0000