aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/search.ml
Commit message (Expand)AuthorAge
* Removing the convenience functions from the Search API.Gravatar Pierre-Marie Pédrot2016-06-07
* avoid communicating to the serarch interface using raw strings.Gravatar Gregory Malecha2016-04-24
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | search: Add an output-name-only search optionGravatar Clément Pit--Claudel2015-07-27
|/
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-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
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Matching patterns: fixed allow_partial_app which was not working onGravatar herbelin2013-04-17
* Exporting the SearchAbout filter.Gravatar ppedrot2013-04-02
* Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?Gravatar ppedrot2013-03-19
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Added a CString module.Gravatar ppedrot2012-11-13
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* When asked for a SearchAbout request, Coq now returns a more preciseGravatar ppedrot2012-09-09
* Updating headers.Gravatar herbelin2012-08-08
* Moved code out of ide_slave in a more appropriate place.Gravatar ppedrot2012-07-09
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* Filter out admitted subgoals from search resultsGravatar glondu2011-02-25
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Filter out "_subproof" objects from search resultsGravatar puech2010-03-11