aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
Commit message (Expand)AuthorAge
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* * Fixed constr_cmp again to handle universes subtyping correctlyGravatar puech2008-10-09
* Fixing constr_cmp, propagating subtyping only right of a productGravatar puech2008-10-02
* Fix a bug, in fold_constr_with_binders, the types of fixpoints wereGravatar msozeau2008-09-13
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
* Backport r11289.Gravatar msozeau2008-07-29
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Confusion sur le paramètre à donner à concrete_name lors du commit 9450Gravatar herbelin2006-12-14
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Mise en conformité de l'ordre des occurrences de pattern avec l'affichageGravatar herbelin2006-02-07
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* Added subtac contrib.Gravatar coq2005-05-25
* Ajout it_mkNamedProd_wo_LetInGravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)Gravatar herbelin2004-08-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* preparation pour release (suite)Gravatar barras2004-03-15
* Deplacement array_map_left and co dans UtilGravatar herbelin2004-02-13
* Prise en compte des defs syntaxiques dans is_global et global_reference qui p...Gravatar herbelin2003-11-24
* Deplacement de iter_constr_with_full_binders dans TermopsGravatar herbelin2003-10-22
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
* Le nom '_' n'est plus valable en v8 pour nommer les variablesGravatar herbelin2003-10-02