aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...Gravatar herbelin2001-03-05
* uniformisation avec constr des lieurs dans rawterm/patternGravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Bug prédicatGravatar herbelin2000-12-25
* Amélioration message d'erreur mauvais prédicatGravatar herbelin2000-12-18
* Suppression du warning several default clausesGravatar herbelin2000-12-16
* Bugs calcul du prédicat des Cases et CaseGravatar herbelin2000-12-15
* Mauvais env donné à new_isevarGravatar herbelin2000-12-14
* Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...Gravatar herbelin2000-12-14
* Bug Cases en presence d'une absence de clauseGravatar herbelin2000-12-05
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage des find_m*typeGravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Correction de bugs (alias initiaux et ordre des cas par défaut)Gravatar herbelin2000-10-10
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en App; Suppression castGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Extension de l'inférence des types des lambdas du prédicatGravatar herbelin2000-06-29
* BugsGravatar herbelin2000-06-09
* bugs infrence des arguments manquants dans le prdicatGravatar herbelin2000-06-02
* Bugs et simplifications coercionsGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* pattern-matching non-exhaustif (occur_rawconstr)Gravatar filliatr2000-05-02
* Retrait fullmind de inductive_summary pour simplicitéGravatar herbelin2000-04-27
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...Gravatar herbelin2000-03-21
* Qqes bugs (evars dans le predicat; tag des cas défauts)Gravatar herbelin2000-03-16
* Reparation bug isevars dans pretypingGravatar herbelin2000-03-10
* Un nouveau moteur pour Cases (phase 1)Gravatar herbelin2000-03-08
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Correction pbs liés aux evarGravatar herbelin2000-01-07
* Bug liftGravatar herbelin1999-12-15
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Poursuite intégration du CasesGravatar herbelin1999-12-13
* Intégration initiale du CasesGravatar herbelin1999-12-11
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 12:48:49 +0000