aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-07gitlab: install num for all jobsGaëtan Gilbert
Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
2018-03-06Merge PR #6917: Fix failing packaging job.Maxime Dénès
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Maxime Dénès
a record.
2018-03-06Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Maxime Dénès
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05Fix failing packaging job.Théo Zimmermann
gtksourceview depends transitively on py2cairo which was updated in Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714): this makes the python3 install step impossible. We also remove the libxml2 install step which was failing in a non-fatal way.
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04Proofview: V82.tactic option to not normalize evarsEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed.
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-04reductionops: remove dead code "bind_assum"Enrico Tassi
2018-03-04proofview: debug API to print a goalEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵Maxime Dénès
coretactics.ml4.
2018-03-04Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from ↵Maxime Dénès
replay nodes]
2018-03-04Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Maxime Dénès
2018-03-04Merge PR #6882: Harden gitattributes against core.whitespace configuration.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵Maxime Dénès
size.
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵Maxime Dénès
supported scenarios.
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid.
2018-03-03Adding a test file for evar handling in the VM.Pierre-Marie Pédrot
2018-03-03Handling evars in the VM.Pierre-Marie Pédrot
We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659.
2018-03-03[compat] Remove "Tactic Pattern Unification"Emilio Jesus Gallego Arias
Following up on #6791, we remove the option "Tactic Pattern Unification"
2018-03-03[compat] Remove "Intuition Iff Unfolding"Emilio Jesus Gallego Arias
Following up on #6791, we remove the option "Intuition Iff Unfolding"
2018-03-03[compat] Remove "Injection L2R Pattern Order"Emilio Jesus Gallego Arias
Following up on #6791, we remove the option "Injection L2R Pattern Order".
2018-03-02CHANGES entry for #6791.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
Fix new deprecation warnings in the standard library.
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5.
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
This simplifies the representation of values, and brings it closer to the ones of the native compiler.
2018-03-02[stm] Partial fix for bug #6884 [location missing from replay nodes]Emilio Jesus Gallego Arias
Example not yet fixed by this patch: ``` Definition u : Type. Definition m : Type. exact nat. Defined. exact bool. Defined. ```
2018-03-01Harden gitattributes against core.whitespace configuration.Gaëtan Gilbert
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
Noticed by Sigurd Schneider.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 13:34:23 +0000