aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* 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
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
* Actually using the domain function for maps.Gravatar ppedrot2013-08-25
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
* Removing association lists in Constrintern.Gravatar ppedrot2013-08-07
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Replacing an association list by a map in globalizing environment.Gravatar ppedrot2013-08-03
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* More dynamic argument scopesGravatar letouzey2013-07-17
* Removing SortArgType.Gravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Using functors to reduce the boilerplate used in registeringGravatar ppedrot2013-06-30
* Removed the distinction between generic Ltac vars and Let/IntroGravatar ppedrot2013-06-27
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Useless use of maps in constr internalizing.Gravatar ppedrot2013-06-25
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Moving wit_unit to Stdarg.Gravatar ppedrot2013-06-19
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
* Implementing a new interface for Genarg, with centralized dataGravatar ppedrot2013-06-18
* Now glob_sign and interp_sign only depend on structures definedGravatar ppedrot2013-06-18
* Added Genarg as generic argument type.Gravatar ppedrot2013-06-12
* Changing the type of Ltac values. Now they are toplevel genericGravatar ppedrot2013-06-12
* More comments in Genarg.Gravatar ppedrot2013-06-06
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Modest protection against "injection" and co raising anomaly inGravatar herbelin2013-06-02
* Removing useless uses of Gmap.Gravatar ppedrot2013-05-14
* Getting rid of module Gmapl.Gravatar ppedrot2013-05-09
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Removing Gmap from Notations.Gravatar ppedrot2013-05-09
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
* Alert when using ".." outside a Notation command.Gravatar herbelin2013-05-08