aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac
AgeCommit message (Expand)Author
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-02-28Add a flag to hide obligations in Program-generated terms under anmsozeau
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-13Remove an unused function with a Evd.fold in subtacletouzey
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-11-07Add information of localisation when an error involving an "implicitherbelin
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
2010-10-12Fix bug #2393: allow let-ins inside telescopes (only fails when there'smsozeau
2010-10-07Fix bug# 2392msozeau
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-27Minor fixes:msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-15Oops, don't use zeta by default.msozeau
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-08Consider OccurCheck a catchable exception.msozeau
2010-03-07Reorder resolution of type class and unification constraints.msozeau
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
2010-02-16Fix sort_dependencies for good, maintaining the initial order.msozeau
2010-02-10Fix [Existing Class] impl and add documentation. Fix computation of themsozeau
2010-01-28Backport fixes in Instance declarations to Program Instance.msozeau
2010-01-26Add [Next Obligation with tactic] support (wish #1953).msozeau
2010-01-14Fix bug #2086, error message when we match on an non-inductive type.msozeau
2010-01-14- Show Obligation Tacticmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:39:17 +0000