aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/smartlocate.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
* Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
* Change [Hints Resolve] to still accept constrs as argumentsGravatar msozeau2012-10-31
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Fixed a bug when reporting unexisting reference to an inductiveGravatar herbelin2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 06:47:11 +0000