aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.mli
Commit message (Expand)AuthorAge
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added rudimentary support for using constructors from the explicitGravatar herbelin2010-06-12
* Fix bug 2307Gravatar pboutill2010-05-20
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22
* DISCLAIMERGravatar puech2009-01-17
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* fixing problem with CompCert: reordering resulting from tac change was not cl...Gravatar barras2008-11-27
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* 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
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* - 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
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 04:36:28 +0000