aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
Commit message (Expand)AuthorAge
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* More on printing references applied to implicit arguments.Gravatar Hugo Herbelin2014-09-16
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Fix bug #3591: print differently eta-expanded projection implicit application...Gravatar Matthieu Sozeau2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Spotted a source of failure of the constr printer in debugger.Gravatar Hugo Herbelin2014-08-18
* Fix non-printing of coercions for primitive projections (fixes bug #3433).Gravatar Matthieu Sozeau2014-08-14
* Change internalization of primitive projections to allow parsing [p t] asGravatar Matthieu Sozeau2014-08-08
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Consistent pretty-printing of primitive projections and their expanded forms.Gravatar Matthieu Sozeau2014-07-31
* Fix printing of projections with implicits.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Now printing body of abbreviations (i.e. notation with a name) withGravatar herbelin2013-05-05
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Fixup notation printing in patternsGravatar pboutill2013-01-07
* Modulification of identifierGravatar 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
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Fix ocamldebug constr printerGravatar pboutill2012-11-28
* Fixed a monomorphization error.Gravatar ppedrot2012-11-26
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* Added a CString module.Gravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Fixed bug #2895Gravatar ppedrot2012-09-09
* Updating headers.Gravatar herbelin2012-08-08
* Fixing bug #2835 (the rationale for printing notations was notGravatar herbelin2012-07-21
* Fixup implicits in patterns & notationsGravatar pboutill2012-07-20
* Bug 2838: ExplApp in mutual inductive parametersGravatar pboutill2012-07-12