aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-12-16Adapting coqide to my last commit: courtieu
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...ppedrot
2011-12-14Some extra universe refreshing seems needed in abstract_generalizeherbelin
2011-12-12CHANGES: some more updatesletouzey
2011-12-12Proof using ...gareuselesinge
2011-12-10Extraction: only do the test on generalizable lets for ocamlletouzey
2011-12-08Makefile: force the installation of all .cmi (and remove some obsolete .mli)letouzey
2011-12-08Extraction: avoid internal eta-reduction (fix #2570)letouzey
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-12-07Html page titlespboutill
2011-12-07Vectors use a bit more the pattern matching compilerpboutill
2011-12-07Typopboutill
2011-12-06Fixed a synchronization bug between coqtop and the CoqIDE command pane.ppedrot
2011-12-06fix Makefile.common handling of -byte-onlygareuselesinge
2011-12-06Documentation of Arguments + implicitsgareuselesinge
2011-12-06Documentation for Arguments + notation scopesgareuselesinge
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 04:22:14 +0000