aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2004-09-12inclusion de meta_map dans evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10simplification de clenvbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08unification encore...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08petit bug avec les effets de bordsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6078 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient ↵herbelin
incorrects: 0 au lieu de 1 et lv dans le mauvait sens) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6075 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06mimick: unify types before making assignationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6067 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06bad env in mimick codebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6065 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03deplacement de clenv vers pretypingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Expansion du prédicat du 'match' vis à vis de la dépendance en le terme ↵herbelin
filtré (utilisation de Anonymous pour signaler une dépendance formelle, en relation avec le nommage dans Inductiveops.type_case_branches); uniformisation/nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6032 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Prise en compte expansion du prédicat du 'match' vis à vis de la ↵herbelin
dépendance en le terme filtré (cf Indrec) + déplacement routines pour Cases à la V7 dans Pretyping) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6031 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵herbelin
inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus ↵herbelin
au moment de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5911 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #794: conv made in wrong envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5897 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #790: better error_not_cleanbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5896 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Eta-expansion du predicat dans build_indrec (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5887 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Eta-expansion du predicat pas seulement pour make_case mais aussi pour ↵herbelin
build_indrec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5884 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ↵herbelin
(c'est au moment de la construction dans Indrec qu'il faut eta-expanser -cf bug #784) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5883 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30updated printing of evar context (may loop ?)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5853 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Double bug d'affichage des cases dépendants (bug #784)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5837 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27Correction affichage v8 des records avec let (bug #798)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5830 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-14test de conversion laissait echapper exception NotConvertiblebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5716 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-29Prise en compte d'un type dont la sorte est une evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5710 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-27Correction incapacité à gérer les annotations de type dépendantes pour ↵herbelin
le if-then-else git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5706 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Correction confusion entre la dependance en les termes filtrees dans ↵herbelin
l'annotation donnee par l'utilisateur et l'annotation utilisee en interne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5668 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07bug #606: mis un message d'erreur plus clairbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5653 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-05Déclaration des record au chargement (ce n'est pas une question de ↵herbelin
visibilité mais d'interprétation au niveau global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5637 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5596 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵herbelin
sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24bug de PP des fix (coqbugs #574)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5550 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation pour release (suite)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5497 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-09bug affichage des cofixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5442 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-08correction de bugs des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27Erreur de Bruijn et oubli substitution alias dans annotation du 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5391 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Inclusion des annotations de type des filtrages dans 'Set Printing All'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5384 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-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-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-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-05On s'affranchit de l'information inductif ou pas dans le prédicat (càdherbelin
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
2004-02-05Suppression des types dans la signature du predicat (ils sontherbelin
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
2004-02-04Reconnaissance précoce de la dépendance du prédicat en un terme filtréherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 11:26:49 +0000