aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.mli
Commit message (Expand)AuthorAge
* 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
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
* É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
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Added subtac contrib.Gravatar coq2005-05-25
* Ajout it_mkNamedProd_wo_LetInGravatar herbelin2005-02-18
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* 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
* 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
* Export is_section_variableGravatar herbelin2003-10-13
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
* Changement de l'afficheur pour que les variables liées aient un nom indépen...Gravatar herbelin2003-09-23
* Deplacement de Declare vers TermopsGravatar herbelin2003-09-13
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* *** empty log message ***Gravatar barras2003-03-12
* Allègement du noyauGravatar herbelin2002-11-18
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Prise en compte des dependances dans la tactique CaseGravatar mohring2002-03-26
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* substitution et pattern modulo letGravatar barras2002-02-11
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Amélioration affichage échec lookup_eliminatorGravatar herbelin2002-01-17
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05