aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2004-02-04Localisation un tout petit peu moins abstraite des erreurs de garde, mais ↵herbelin
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
2004-02-03Relachement condition pour declarer un inductif dans la table des 'If'; ↵herbelin
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
2004-02-03Backtrack sur recuperation de noms a partir du type, car casse la correction ↵herbelin
des dependances de nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5283 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute ↵herbelin
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
2004-01-29Reparation d'une rupture (en presence de types implicites) de l'invariant ↵herbelin
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
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵herbelin
paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-12Set is not always impredicativebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5194 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-27Type le 'return' comme un typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5154 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Affichage opaqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5133 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Substitution dans REvar; reparation bug 277herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5115 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application ↵herbelin
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
2003-12-17Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5109 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16Correction bug 371 (sub_match retournait des instances non closes)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5106 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵herbelin
passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Bug introduit avec le 'Simpl f'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Ajout 'Simpl f'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4948 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Ajout mis_constructor_nargs_envherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4936 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Ajout reduce_to_quantified_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4835 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Amelioration message d'erreur pour ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4789 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Deplacement de iter_constr_with_full_binders dans Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4705 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Export is_section_variableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4622 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Le nom '_' n'est plus valable en v8 pour nommer les variablesherbelin
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
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4499 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom ↵herbelin
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
2003-09-13Deplacement de Declare vers Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵herbelin
interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12open superfluherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4356 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Bug predicat old Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4345 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Bug predicat let-tupleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4338 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4280 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug et améliorations diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug détypage du fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4262 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
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
2003-06-11Pb quand une meme classe est definie dans 2 fichiersherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4138 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Simplification case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4114 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Factorisation de detype_case pour utilisation par l'afficheur de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4113 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4110 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Preservation affichage des ?n en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Rien d'importantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4009 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 04:20:38 +0000