aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix printing of projections with implicits.Gravatar Matthieu Sozeau2014-05-06
* Fix inversion of notations for projections.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Dumpglob: factor out reference dumping.Gravatar Carst Tankink2014-04-10
* Better error message when found more than once object of name ...Gravatar Pierre Boutillier2014-04-02
* Fixing interpretation of tactics in terms. It was forgetting part of theGravatar Pierre-Marie Pédrot2014-03-06
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Removing generic equality in Syntax plugin.Gravatar Pierre-Marie Pédrot2014-03-02
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Better behaviour for sets of reserved names.Gravatar Pierre-Marie Pédrot2014-03-01
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
* Fix grammatical mistake in error message (bug #3238)Gravatar xclerc2014-02-24
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
* Fixing an interpretation bug with tactics in notations. For some obscureGravatar Pierre-Marie Pédrot2014-01-19
* Disable GlobRef feedback (CoqIDE does nothing with them)Gravatar Enrico Tassi2014-01-05
* Notation variables are now taken into account as possible ltac bound variablesGravatar Pierre-Marie Pédrot2013-12-22
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Adding the necessary hooks to handle tactics in terms.Gravatar Pierre-Marie Pédrot2013-11-27
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Fixing bug #3165.Gravatar Pierre-Marie Pédrot2013-11-23
* Reverting the old LIFO behaviour of the notation finding algorithm.Gravatar ppedrot2013-11-08
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Restore my version of notation_ops.ml now that List.remove_assoc_f is fixedGravatar letouzey2013-10-24
* Oups, repair the compilation (micromega + Morphism_prop)Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Some more hand-written comparison functions to avoid polymorphic comparison.Gravatar xclerc2013-10-14
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 15:31:17 +0000