aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Plus d'explicitation d'un message d'erreurGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation erreur interp_notationGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | 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
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | 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
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | 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
* Mauvaise dependance en states7/initial.coqGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation erreur interp_notationGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug affichage en presence de '{ _ }'Gravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5323 85f007b7-540e-0410-9357-904b9bb8a0f7
* lazy was translated to cbv, obviously wrongGravatar bertot2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout delimiteur pour bool_scopeGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5321 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Décomposition automatique des règles d'analyse syntaxique pour lesGravatar herbelin2004-02-12
| | | | | | | | | | | 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
* Implicits can have an optional list of argument, which is differentGravatar bertot2004-02-12
| | | | | | | | | 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
* majGravatar filliatr2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5317 85f007b7-540e-0410-9357-904b9bb8a0f7
* a new version that uses intro patterns, but the code still needs some cleaningGravatar bertot2004-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5316 85f007b7-540e-0410-9357-904b9bb8a0f7
* removes a lot comments that may be useful for later code maintenance, butGravatar bertot2004-02-11
| | | | | | | 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
* majGravatar filliatr2004-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of a bug in Functional Scheme discovered when porting theGravatar coq2004-02-10
| | | | | | | contrib QArith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5313 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack implicit dans BvectorGravatar marche2004-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5312 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5311 85f007b7-540e-0410-9357-904b9bb8a0f7
* New version of Functional Scheme and functional induction. Deals withGravatar coq2004-02-09
| | | | | | | | 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
* patch Bvector: args implicitesGravatar marche2004-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5309 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5308 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5307 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5306 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test dependencies in constructorsGravatar herbelin2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5304 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de bugs de congruence et firstorder (inductifs)Gravatar corbinea2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout filtrage sur motifs dépendants dans des inductifs différentsGravatar herbelin2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5302 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5300 85f007b7-540e-0410-9357-904b9bb8a0f7
* On s'affranchit de l'information inductif ou pas dans le prédicat (càdGravatar herbelin2004-02-05
| | | | | | | | | fusion de PrLetIn et PrNotInd); cela permet de traiter des cas de motifs dans des types dépendants ne se réduisant pas dans le même inductif (cf coqbugs #207) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des types dans la signature du predicat (ils sontGravatar herbelin2004-02-05
| | | | | | | retrouvés via les types des termes à filtrer) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5298 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5297 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reconnaissance précoce de la dépendance du prédicat en un terme filtréGravatar herbelin2004-02-04
| | | | | | | | dans le cas v8 (build_initial_predicate au lieu de expand_arg); Correction d'un bug en présence de termes de type non inductif (cf success/Case15.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification de la prise en compte des termes de type non inductifGravatar herbelin2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5294 85f007b7-540e-0410-9357-904b9bb8a0f7
* clean-ide plus precisGravatar herbelin2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation un tout petit peu moins abstraite des erreurs de garde, mais ↵Gravatar herbelin2004-02-04
| | | | | | reste a transporter les loc dans check_fix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Boite autour des quote pour eviter un retour a la ligne apres le premier ↵Gravatar herbelin2004-02-04
| | | | | | guillement; quote seulement en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5291 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug fix find coqideGravatar coq2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5290 85f007b7-540e-0410-9357-904b9bb8a0f7
* highlightGravatar marche2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5289 85f007b7-540e-0410-9357-904b9bb8a0f7
* search windowGravatar coq2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5287 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relachement condition pour afficher @ en cas d'explicitation d'implicitesGravatar herbelin2004-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relachement condition pour declarer un inductif dans la table des 'If'; ↵Gravatar herbelin2004-02-03
| | | | | | contrainte de non dependances en les args des constructeurs pour avoir un affichage spontane avec if-then-else git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur recuperation de noms a partir du type, car casse la correction ↵Gravatar herbelin2004-02-03
| | | | | | des dependances de nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug focusGravatar herbelin2004-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre noms de variable indefinis et guillemets autour des constrGravatar herbelin2004-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un ↵Gravatar herbelin2004-02-03
| | | | | | nom doit filtrer un nom et anonymous doit filtrer anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5280 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 14:32:19 +0000