aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Deplacement array_map_left and co dans UtilGravatar herbelin2004-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5343 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug numerotation des occurrences pour 'simpl id at n' (suite)Gravatar herbelin2004-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug numerotation des occurrences pour 'simpl id at n' (2 protections ↵Gravatar herbelin2004-02-13
| | | | | | maintenant !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5336 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
* 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
* 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
* 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
* Ajout option raw_print (Set Printing All) pour desactiver toute ↵Gravatar herbelin2004-01-29
| | | | | | fonctionnalite de haut niveau de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation d'une rupture (en presence de types implicites) de l'invariant ↵Gravatar herbelin2004-01-29
| | | | | | que les variables liees sont toujours nommees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵Gravatar herbelin2004-01-27
| | | | | | paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Set is not always impredicativeGravatar barras2004-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type le 'return' comme un typeGravatar herbelin2003-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage opaqueGravatar herbelin2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Substitution dans REvar; reparation bug 277Gravatar herbelin2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Substitution dans REvar et PEvar plutot que encodage via noeud application ↵Gravatar herbelin2003-12-19
| | | | | | pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'Gravatar herbelin2003-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 371 (sub_match retournait des instances non closes)Gravatar herbelin2003-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵Gravatar herbelin2003-11-24
| | | | | | passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Simpl f'Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement subst_rawconstr dans RawtermGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mis_constructor_nargs_envGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout reduce_to_quantified_refGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration message d'erreur pour ltacGravatar herbelin2003-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de iter_constr_with_full_binders dans TermopsGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export is_section_variableGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le nom '_' n'est plus valable en v8 pour nommer les variablesGravatar herbelin2003-10-02
| | | | | | | dépendantes qui par hasard aurait été déclarées Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseGravatar herbelin2003-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de l'afficheur pour que les variables liées aient un nom ↵Gravatar herbelin2003-09-23
| | | | | | indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de Declare vers TermopsGravatar herbelin2003-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵Gravatar herbelin2003-09-12
| | | | | | interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
* open superfluGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug predicat old CaseGravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug predicat let-tupleGravatar herbelin2003-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place possibilité de définitions locales dans les paramètres des ↵Gravatar herbelin2003-09-06
| | | | | | inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
* V8: FUNCLASS -> Funclass, SORTCLASS -> SortclassGravatar herbelin2003-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug et améliorations diversesGravatar herbelin2003-08-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug détypage du fixGravatar herbelin2003-08-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4262 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
| | | | | | | | | | | | | | Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pb quand une meme classe est definie dans 2 fichiersGravatar herbelin2003-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification case_infoGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation de detype_case pour utilisation par l'afficheur de patternGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration afficheur de Cases pour les constr_patternGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4110 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-21 18:13:54 +0000