aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* MAJGravatar herbelin2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@407 85f007b7-540e-0410-9357-904b9bb8a0f7
* retour a la version qui ne contournait pas le bug de PatternMatchingFailure ↵Gravatar herbelin2000-05-03
| | | | | | non trappe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@406 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de Fw pour les implicitesGravatar herbelin2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout get_referenceGravatar herbelin2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de ↵Gravatar herbelin2000-05-03
| | | | | | conclPattern soit rattrapable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@403 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage de certains printersGravatar herbelin2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
* construct_reference prend en compte aussi les variables du contextGravatar filliatr2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@399 85f007b7-540e-0410-9357-904b9bb8a0f7
* pattern-matching non-exhaustif (occur_rawconstr)Gravatar filliatr2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@398 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Problème avec SOPATTGravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Problème avec motif du second-ordreGravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite intégration de constr_patternGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@392 85f007b7-540e-0410-9357-904b9bb8a0f7
* MODIFS pour compatibilité aussi 2.99Gravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration progressiveGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage Error et ValueGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@388 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@387 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage bdize -> ast_of_constrGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@385 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
| | | | | | | | | Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
| | | | | | | | | Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@382 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage Omega (code seulement)Gravatar filliatr2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise sous CVS d'OmegaGravatar filliatr2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@380 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage en ocaml / camlp4 3.00Gravatar filliatr2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@379 85f007b7-540e-0410-9357-904b9bb8a0f7
* chgt unify_0Gravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@378 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait fullmind de inductive_summary pour simplicitéGravatar herbelin2000-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@376 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression doublonGravatar filliatr2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Débranchement provisoire equality et tautoGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@374 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@373 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@371 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage ancien pattern en cases_patternGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@370 85f007b7-540e-0410-9357-904b9bb8a0f7
* N'importe quel rawconstr maintenant dans le contexte d'une référenceGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@367 85f007b7-540e-0410-9357-904b9bb8a0f7
* discharge des axiomesGravatar filliatr2000-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation pbs (coqc not finding coqtop, coqc not finding .vo whenGravatar courant2000-04-21
| | | | | | | building states, coqc wrongly giving option -bindir to coqtop) fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@365 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sign.db_signature is now an abstract typeGravatar courant2000-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte du renommage des fonctions de AsttermGravatar herbelin2000-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Portage (pour la forme) de minicoqGravatar herbelin2000-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@360 85f007b7-540e-0410-9357-904b9bb8a0f7
* erreurs lexicales dans les patterns (manquait des espaces)Gravatar filliatr2000-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@359 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réajout globalize_commandGravatar herbelin2000-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@358 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-09 21:03:40 +0000