| Age | Commit message (Expand) | Author |
|---|
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-11-04 | Auto: removal of ?use_core_db obsolete now that we have nocore | letouzey |
| 2011-10-26 | Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo | letouzey |
| 2011-10-18 | Fix bug #2227 | msozeau |
| 2011-09-23 | auto with nocore : disable the use of the core database (wish #2188) | letouzey |
| 2011-04-20 | This is used in the rippling plugin. This also allows fixing bug #2188. | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-04 | - Allow to set a particular transparent_state for the local hint | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-10-31 | An experimental support for open constrs in hints and in "using" | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | 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 |
| 2009-12-24 | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-22 | Better use of transparency information for local hypotheses: | msozeau |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-03-31 | Fix auto so that Extern tactics associated to no patterns can apply to | msozeau |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 2008-09-07 | 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-04 | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau |
| 2008-08-27 | Little cleanup in auto. | msozeau |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-06-27 | Enhanced discrimination nets implementation, which can now work with | msozeau |
| 2008-04-29 | Fix eauto still using delta when it shouldn't (should make CoRN compile | msozeau |
| 2008-04-28 | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau |
| 2008-04-27 | - Fix bug in unification not taking into account the right meta | msozeau |
| 2008-04-21 | - Parameterize unification by two sets of transparent_state, one for open | msozeau |
| 2008-04-04 | Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand | herbelin |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2006-01-28 | 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-24 | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2004-12-07 | * added subst_evaluable_reference | sacerdot |
| 2004-12-07 | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-09-10 | simplification de clenv | barras |
| 2004-09-08 | unification encore... | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-06-14 | Ajout option Local à Hint, Hints et HintDestruct | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
