aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
Commit message (Expand)AuthorAge
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Removing SortArgType.Gravatar ppedrot2013-07-05
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Removed the ad-hod handling of wit_tacticn.Gravatar ppedrot2013-07-02
* Fixing Camlp4 compilation.Gravatar ppedrot2013-06-30
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Fixing argument extension. Instead of qualified names, stringGravatar 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
* Added Genarg as generic argument type.Gravatar ppedrot2013-06-12
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Make ist (interp_sign) available to TACTIC EXTEND codeGravatar gareuselesinge2013-05-29
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
* Fix some camlp5 quotations , restoring compatibility with camlp5 5.xGravatar letouzey2013-03-17
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Added exception enrichment. Now one can define additional arbitraryGravatar ppedrot2013-02-18
* Added backtrace primitives.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
* Using library string functions.Gravatar ppedrot2012-12-13
* More monomorphizationsGravatar ppedrot2012-11-13
* Added a CString module.Gravatar ppedrot2012-11-13
* Added an Int module with dummy utility functions.Gravatar ppedrot2012-11-08
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* Continue killing hidden tactics : no more generated h_xxxGravatar letouzey2012-10-15
* Stylistic improvement: avoid a "if match List.hd"Gravatar letouzey2012-10-15
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Argextend: avoid useless "open Extrawit"Gravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01