aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
2016-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-04-05Revert "Prevent pretyping from checking well-guardedness unnecessarily."Arnaud Spiwack
2015-09-25Show assumptions of well-foundedness in `Print Assumptions`Arnaud Spiwack
2015-09-25Add a field in `constant_body` to track constant whose well-foundedness is as...Arnaud Spiwack
2015-09-25Declare assumptions of well-founded definitions as unsafe.Arnaud Spiwack
2015-09-25Prevent pretyping from checking well-guardedness unnecessarily.Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-25Add (temporary) syntax for assuming guardedness in (co-)fixed points.Arnaud Spiwack
2015-09-25Add `Guarded` to the assumption tokens.Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-06-25Add coqide syntax highlighting for `Assume`.Arnaud Spiwack
2015-06-25Adjust checker after `Assume [Positive]`.Arnaud Spiwack
2015-06-24Make inductives that were assumed positive appear in `Print Assumptions`.Arnaud Spiwack
2015-06-24When assuming an inductive type positive, then it is declared "unsafe" to the...Arnaud Spiwack
2015-06-24Add syntax entry to assume strict positivity of an inductive type.Arnaud Spiwack
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 2).Arnaud Spiwack
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 1).Arnaud Spiwack
2015-06-24Add a field in `mutual_inductive_body` to represent mutual inductive whose po...Arnaud Spiwack
2015-06-24Extend test-suite for the positivity checker.Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
2015-06-24improve --help documentation: the -m|--memory option was missingGabriel Scherer
2015-06-24when OCAML_GC_STATS points to a filepath, write Gc stats into itGabriel Scherer
2015-06-24On-demand Require.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-23obligations: wrap Ephemeron.get to make error more informativeEnrico Tassi
2015-06-23Wrap the program_info type up in the ephemeron mechanismAlec Faithfull
2015-06-23Fixing incompatibility introduced with simpl in commit 364decf59c1 (orHugo Herbelin
2015-06-23Less closures makes the GC happy.Pierre-Marie Pédrot
2015-06-23Wrapped the declare_object function to pretty-print anomalies at loading time.Thomas Sibut-Pinote
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-23Add a Set Dump Bytecode command for debugging purposes.Maxime Dénès
2015-06-23Fix `Pp` function used by the `Info` command.Arnaud Spiwack
2015-06-23With the field record punning syntax.Theo Zimmermann
2015-06-23Put all arguments of strategy in record.Theo Zimmermann
2015-06-23Strategy is now a record type with a function field.Theo Zimmermann
2015-06-23Add comments.Theo Zimmermann
2015-06-23Warning are enabled by default in interactive mode.Pierre-Marie Pédrot
2015-06-23Document the positivity checker.Arnaud Spiwack
2015-06-22Merge branch 'v8.5' into trunkPierre Letouzey
2015-06-22Remove uses of polymorphic equality from prev. commitClément Pit--Claudel
2015-06-22Replace 'try ... with Failure "List.last"' with 'if l <> []'Clément Pit--Claudel
2015-06-22Guard the List.hd call in [Show Intros]Clément Pit--Claudel
2015-06-22Add efficient extraction of [nat], [Z], and [string] to HaskellNickolai Zeldovich
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-22Fixup last commitPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 17:31:02 +0000