aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-02-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5359 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-18Bug coercions imbriquees + suppression des coercions avant filtrage sur ↵herbelin
notations pour respecter le cpmt v7 et la symtrie avec le parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5357 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5356 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-17Ajout de lconstr, constr et binder_constr dans Print Grammar constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5354 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5353 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16Erreur dépendance en Util lui-mêmeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5351 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-16export the general function for getting information from the environmentbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5347 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5346 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5345 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5344 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13Deplacement array_map_left and co dans Utilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5343 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13Ajout array_map_left and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5342 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13Uniformisation du comportement de Notation et Reserved Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5341 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et ↵herbelin
Reserved Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5340 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-13Bug numerotation des occurrences pour 'simpl id at n' (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5338 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-13Bug numerotation des occurrences pour 'simpl id at n' (2 protections ↵herbelin
maintenant !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5336 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-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5333 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5332 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5331 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Plus d'explicitation d'un message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5330 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation erreur interp_notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5329 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
dans le module de leur définition. Correction bug de nommage de la notation en présence de "{ _ }" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5327 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
dans le module de leur définition. Internalisation des preident comme des noms qui ne sont pas des références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5326 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Mauvaise dependance en states7/initial.coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5325 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation erreur interp_notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Correction bug affichage en presence de '{ _ }'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5323 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-12Ajout delimiteur pour bool_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5321 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5320 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A*{B}+{C}" en présence d'une notation "_ * { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 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-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5317 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-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5314 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-10backtrack implicit dans Bvectormarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5312 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5311 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-09patch Bvector: args implicitesmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5309 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:55:54 +0000