aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-11-11Prehistory of Coq: consistency.Arnaud Spiwack
2015-11-11Prehistory of Coq: various corrections on English.Arnaud Spiwack
2015-11-11Prehistory of Coq: asciidoc conversion.Arnaud Spiwack
2015-10-28Fixing the return type of the Atoken symbol.Pierre-Marie Pédrot
2015-10-28Type-safe Argextend.Pierre-Marie Pédrot
2015-10-27Removing unused code in Pcoq.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Getting rid of most uses of unsafe_grammar_extend.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.make_rule.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-27Type-safe grammar extensions.Pierre-Marie Pédrot
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-25Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Pierre Letouzey
2015-10-25Getting rid of the Atactic entry.Pierre-Marie Pédrot
2015-10-25Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Pierre Letouzey
2015-10-25Minor module cleanup : error HigherOrderInclude was never happeningPierre Letouzey
2015-10-25Getting rid of the Agram entry.Pierre-Marie Pédrot
2015-10-24Fixing a loop in checking hints with holes.Hugo Herbelin
2015-10-24Backtracking on interpreting toplevel calls to exact in scope determinedHugo Herbelin
2015-10-23Support "Functional Scheme" in coqdoc. (Fix bug #4382)Guillaume Melquiond
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-22Using GADTs in Xmlprotocol.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-10-21Turn Pcoq into a regular ML file.Pierre-Marie Pédrot
2015-10-21Expanding the grammar extensions of Pcoq.Pierre-Marie Pédrot
2015-10-21Removing the dependencies of Pcoq in IFDEF macros.Pierre-Marie Pédrot
2015-10-21Mention bug 3199 fix as a source of incompatibilities.Matthieu Sozeau
2015-10-21Expliciting some uses of Compat module.Pierre-Marie Pédrot
2015-10-21Bug #3956 is fixed.Matthieu Sozeau
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
2015-10-21Fixed (and changed) infoH.Pierre Courtieu
2015-10-20Fix lemma-overloadingMatthieu Sozeau
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Expliciting the uses of the old Tacmach API in Tactics.Pierre-Marie Pédrot
2015-10-19Removing some unsafe uses of monotonicity.Pierre-Marie Pédrot
2015-10-19Do occur-check w.r.t existential's types also when instantiating an evar.Matthieu Sozeau
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-19Categorizing debug messages as such + NonLogical uses loggers.Pierre Courtieu
2015-10-19Test for #4372 (anomaly in inversion in the presence of fake dependency).Hugo Herbelin
2015-10-19More monotonicity in Tactics.Pierre-Marie Pédrot
2015-10-19Turning anomaly into error for #4372 (weakness of inversion in theHugo Herbelin
2015-10-19Removing tclEVARS in various places.Pierre-Marie Pédrot
2015-10-19Reducing the uses of tclEVARS in Tactics by using monotonous functions.Pierre-Marie Pédrot
2015-10-19Adding a monotonic variant of Goal.enter and Goal.nf_enter.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 05:01:42 +0000