aboutsummaryrefslogtreecommitdiff
path: root/test-suite/interactive
AgeCommit message (Collapse)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-06-11[test-suite] [stm] Interactive test case for fail-on-qed.Emilio Jesus Gallego Arias
2019-05-23Fixing typos - Part 3JPR
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
Also make `Check S` no longer anomaly Add a couple more test cases for numeral notations Also add another possibly-confusing error message to the doc. Respond to Hugo's doc request with Zimmi48's suggestion From https://github.com/coq/coq/pull/8064/files#r204191608
2018-08-31WIP: adapt Numeral Notation to synchronized prim notationsPierre Letouzey
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
The first part (e.g. register_bignumeral_interpretation) deals only with the interp/uninterp closures. It should typically be done as a side effect during a syntax plugin loading. No prim notation are active yet after this phase. The second part (enable_prim_token_interpretation) activates the prim notation. It is now correctly talking to Summary and to the LibStack. To avoid "phantom" objects in libstack after a mere Require, this second part should be done inside a Mltop.declare_cache_obj The link between the two parts is a prim_token_uid (a string), which should be unique for each primitive notation. When this primitive notation is specific to a scope, the scope_name could be used as uid. Btw, the list of "patterns" for detecting when an uninterpreter should be considered is now restricted to a list of global_reference (inductive constructors, or injection functions such as IZR). The earlier API was accepting a glob_constr list, but was actually only working well for global_reference. A minimal compatibility is provided (declare_numeral_interpreter), but is discouraged, since it is known to store uncessary objects in the libstack.
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2016-06-06Error box detection run only on errorEnrico Tassi
Advantage: 0 cost if no error occurs Disadvantage: a box *must* end with the error absorbing command
2016-06-06STM: proof block detection made optional + simple testEnrico Tassi
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-07-30Test file for bug #4289 (buggy hash-consing of kernel name pairsHugo Herbelin
breaking backtracking in the presence of functors). In "interactive" rather than "bugs" because of the use of Back.
2014-03-13nanoPG: better copy/pasteEnrico Tassi
2014-01-13rename Paral-ITP demo fileEnrico Tassi
2014-01-13Paral-ITP demo: better commentsEnrico Tassi
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-06fix simple test for paral-itpEnrico Tassi
2013-10-01demo file for paral-itpgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16832 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Trickyer test for Paral-ITPgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Test for Paral-ITPgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16681 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23Correction bug #1229 (toplevel "unresolved evar" fled throughherbelin
Declare Implicit Tactic support) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-01Interactive test of Backherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7486 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:38:03 +0000