aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac
Commit message (Expand)AuthorAge
* Fix camlp4 compilationGravatar pboutill2012-01-31
* Fix for Program Instance not separately checking the resolution of evars of t...Gravatar msozeau2012-01-23
* Another quick hack that works this time, to handle printing of locality in Pr...Gravatar ppedrot2012-01-23
* Reverted previous commit, which broke library compilation.Gravatar ppedrot2012-01-20
* This is a quick hack to permit the parsing of the locality flag in the Progra...Gravatar ppedrot2012-01-20
* Fixed the pretty-printing of the Program plugin.Gravatar ppedrot2012-01-17
* Proof using ...Gravatar gareuselesinge2011-12-12
* Quick hack to avoid anomaly on using Program w/o having required JMeq.Gravatar herbelin2011-11-30
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Fix inductive coercion code in Program (bug #2378)Gravatar msozeau2011-10-18
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
* Fix commit 14489: missing Coq. in dirpathGravatar letouzey2011-09-23
* Program: add some check_required_library (fix #2592) + some dead code removalGravatar letouzey2011-09-23
* Subtac_cases: replaced some generic = on constr by destructorsGravatar puech2011-07-29
* Fix compilation errorGravatar msozeau2011-06-30
* Keep obligation source information in ProgramGravatar msozeau2011-06-30
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Fix bug 2269, program typechecker not used in Instance conclusionsGravatar msozeau2011-06-17
* Call process_vernac_interp_error before calling Errors.print inGravatar herbelin2011-06-10
* Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...Gravatar msozeau2011-06-07
* Fix bug #2415: warn when closing modules or sections and some obligations are...Gravatar msozeau2011-06-07
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
* Extraction: unfolds the let-in created by Program when handling "match"Gravatar letouzey2011-04-07
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Improved define_evar_as_lambda which was creating an unrelated new evarGravatar herbelin2011-03-05
* Add a flag to hide obligations in Program-generated terms under anGravatar msozeau2011-02-28
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* Data structure telling implicits of local variables is a map in theGravatar pboutill2011-02-10
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Remove an unused function with a Evd.fold in subtacGravatar letouzey2010-12-13
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Add information of localisation when an error involving an "implicitGravatar herbelin2010-11-07
* Cleaning the use of parentheses around evd and evdref (cosmetic commit).Gravatar herbelin2010-10-31
* Fix bug #2393: allow let-ins inside telescopes (only fails when there'sGravatar msozeau2010-10-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 06:09:55 +0000