aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-12-06Documentation for Arguments + simplgareuselesinge
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-12-06Backtrack on synchronizing universe counter with resetherbelin
2011-12-05Registering universe and meta/evar counters as summaries so as toherbelin
2011-12-05Yet another fix about alias in testing if pattern unification applies.herbelin
2011-12-04Fixing bugs in doc about when "with" is needed or not to give bindingsherbelin
2011-12-04Fixed a small regression in pattern-matching compilation introduced inherbelin
2011-12-04A small test for type inference (used to be a regression at some time).herbelin
2011-12-04Fixing superflous newline in output of About when no parameter is renamed.herbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-30Fixed a bug introduced in r12755. CoqIDE would ignore the Printing Existentia...ppedrot
2011-11-30Extraction: try to avoid issues with an Include directly inside a .vletouzey
2011-11-30Now CoqIDE relies on the option query mechanism to set printing options. Stil...ppedrot
2011-11-30More type safety in query GADT (again).ppedrot
2011-11-30Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...ppedrot
2011-11-30Continuing r14747 being actually incomplete (flushing warnings andherbelin
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
2011-11-30Preventing Implicit Arguments warning to be shown in non verbose modeherbelin
2011-11-29Documentation of appcontextletouzey
2011-11-29Fixed a warning about unused variable introduced in r14731ppedrot
2011-11-29lib/xml_lexer.ml in .gitignore (produced by a .mll)letouzey
2011-11-29Extraction: typo in last commitletouzey
2011-11-29fix for bug #2649corbinea
2011-11-29Term: properly ignore Casts between Apps in constr_ordpuech
2011-11-29Term: useless conversion to list in constr_ord deletedpuech
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
2011-11-28Fixing dependencies postprocessing bug in pattern-matching compilation.herbelin
2011-11-28Term: Fix hash_constr behavior for Cast lnterleaved in application spines.puech
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-28doc: two minor fixes to make my latex happyletouzey
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-25Added an API call to retrieve and change the option stateppedrot
2011-11-25Separated the toplevel interface into a purely declarative module with associ...ppedrot
2011-11-25Cleaning up XML parsingppedrot
2011-11-25avoid relying on weak invariant in cbv.mlbgregoir
2011-11-24Added a function to inspect current option state.ppedrot
2011-11-24Fixed the XML parser CDATA handling (and changed the EOL convention of these ...ppedrot
2011-11-24Fixed some missing options from previous commit.ppedrot
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-24Moving XML handling to lib directoryppedrot
2011-11-24Correct direction for definitional typeclassesmsozeau
2011-11-23In emacs mode, prints a list of the dependent existential variables introducedaspiwack
2011-11-23Adds a pair of function in Evar_util to gather dependent evars in anaspiwack
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21coqide default pref files are by default in /etc/xdg/coq/pboutill
2011-11-21/home/pirbo/.coqrc* are read againpboutill
2011-11-21-user option removalpboutill