| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | locus.mli for occurrences+clauses, misctypes.mli for various little things |  letouzey | 2012-05-29 |
| * | remove undocumented and scarcely-used tactic auto decomp | letouzey | 2012-04-23 |
| * | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey | 2012-03-30 |
| * | Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl | letouzey | 2012-03-30 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | Merge subinstances branch by me and Tom Prince. |  msozeau | 2011-11-17 |
| * | Auto: removal of ?use_core_db obsolete now that we have nocore | letouzey | 2011-11-04 |
| * | Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo | letouzey | 2011-10-26 |
| * | Fix bug #2227 | msozeau | 2011-10-18 |
| * | auto with nocore : disable the use of the core database (wish #2188) | letouzey | 2011-09-23 |
| * | This is used in the rippling plugin. This also allows fixing bug #2188. | msozeau | 2011-04-20 |
| * | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
| * | - Allow to set a particular transparent_state for the local hint | msozeau | 2011-03-04 |
| * | - Fix treatment of globality flag for typeclass instance hints (they | msozeau | 2011-02-14 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | An experimental support for open constrs in hints and in "using" |  herbelin | 2010-10-31 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
| * | Various minor improvements of comments in mli for ocamldoc | letouzey | 2010-04-29 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
| * | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |
| * | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Better use of transparency information for local hypotheses: | msozeau | 2009-09-22 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin | 2009-05-09 |
| * | Fix auto so that Extern tactics associated to no patterns can apply to | msozeau | 2009-03-31 |
| * | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin | 2008-12-26 |
| * | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau | 2008-09-07 |
| * | Fixes in typeclasses resolution. Avoid reducing instances types before | msozeau | 2008-09-07 |
| * | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau | 2008-09-04 |
| * | Little cleanup in auto. | msozeau | 2008-08-27 |
| * | - New auto hints for transparency/opacity control, not bound to | msozeau | 2008-08-22 |
| * | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
| * | Fix eauto still using delta when it shouldn't (should make CoRN compile | msozeau | 2008-04-29 |
| * | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau | 2008-04-28 |
| * | - Fix bug in unification not taking into account the right meta | msozeau | 2008-04-27 |
| * | - Parameterize unification by two sets of transparent_state, one for open | msozeau | 2008-04-21 |
| * | Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand | herbelin | 2008-04-04 |
| * | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau | 2008-03-06 |
| * | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin | 2007-09-30 |
| * | Ajout option 'using lemmas' à auto/trivial/eauto | herbelin | 2006-01-28 |
| * | Suppression code pour hints nommés à la V7 (voire à la V6...) | herbelin | 2006-01-28 |
| * | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin | 2006-01-24 |
| * | Compatibilité ocamlweb pour cible doc | herbelin | 2005-01-21 |
| * | * added subst_evaluable_reference |  sacerdot | 2004-12-07 |
| * | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot | 2004-12-07 |
| * | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot | 2004-11-16 |
| * | simplification de clenv |  barras | 2004-09-10 |
letouzey
pboutill
msozeau
glondu
herbelin
soubiran
sacerdot
barras