aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into ↵Gravatar Hugo Herbelin2016-03-09
|\ \ | | | | | | | | | | | | | | | aspiwack-render-prehistory3 Pull request #120
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-09
|\ \ \ | | |/ | |/|
| * | Fix test-suite file coq-prog-argsGravatar Matthieu Sozeau2016-03-09
| | | | | | | | | | | | They were not parsed correctly with a newline in the middle.
* | | Redo fix init_setoid -> init_relation_classesGravatar Matthieu Sozeau2016-03-09
| | | | | | | | | | | | It got lost during a merge with the 8.5 branch.
| * | Fixed bug #4533 with previous Keyed Unification commitGravatar Matthieu Sozeau2016-03-09
| | | | | | | | | | | | Add test-suite file to ensure non-regression.
| * | Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)Gravatar Enrico Tassi2016-03-09
| | | | | | | | | | | | This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
| * | Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
| | | | | | | | | | | | | | | | | | | | | Try first to find a keyed subterm without conversion/betaiota on open terms (that is the usual strategy of rewrite), if this fails, try with full conversion, incuding betaiota. This makes the test-suite pass again, retaining efficiency in the most common cases.
| * | Adding backtraces to scheme error messages.Gravatar Pierre-Marie Pédrot2016-03-07
| | |
| * | Re-enable OCaml warnings disabled by mistake as part of e759333.Gravatar Maxime Dénès2016-03-07
| | |
* | | Partial disentangling of Ltac codebase.Gravatar Pierre-Marie Pédrot2016-03-06
|\ \ \
| * | | Expurging grammar.mllib from uselessly linked modules.Gravatar Pierre-Marie Pédrot2016-03-06
| | | |
| * | | Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
| | | |
| * | | Putting Tactic_debug just below Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
| | | |
| * | | Removing dependency of Himsg in tactic files.Gravatar Pierre-Marie Pédrot2016-03-06
| | | |
| * | | Moving Tactic_debug to tactics/ folder.Gravatar Pierre-Marie Pédrot2016-03-06
| | | |
| * | | Moving Ltac traces to Tacexpr and Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
|/ / /
* | | Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Gravatar Pierre-Marie Pédrot2016-03-06
| | | | | | | | | | | | | | | | | | | | | | | | We just reuse the same one weird old trick in CAMLP4 to compare keywords and identifiers as tokens. Note though that the commit 982460743 does not fix the keyword vs. identifier issue in CAMLP4, so that the corresponding test fails. This means that since that commit, some code compiling with CAMLP5 does not when using CAMLP4, making it a second-class citizen.
* | | Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
| | |
* | | Splitting the nsatz ML module into an implementation and a grammar files.Gravatar Pierre-Marie Pédrot2016-03-06
| | |
* | | Moving Eauto to a simple ML file.Gravatar Pierre-Marie Pédrot2016-03-06
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
* | | Using build_selector from Equality as a replacement of the selectorGravatar Hugo Herbelin2016-03-05
| | | | | | | | | | | | | | | | | | | | | | | | in cctac which does not support indices properly. Incidentally, this should fix a failure in RelationAlgebra, where making prod_applist more robust (e8c47b652) revealed the discriminate bug in congruence.
* | | Exporting build_selector, a component of discriminate, for use in congruence.Gravatar Hugo Herbelin2016-03-05
| | |
* | | Generalizing the uses of tactic scopes everywhere.Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | This feature allows the user to write "let x := open_constr(foo) in ..." for instance without having to resort to tactic notations. Some changes have been introduced in the parsing of ad-hoc argument scopes, e.g. one has to put parentheses around constr:(...) and ltac:(...) in tactics. This breaks badly written scripts, although it is easy to be forward-compatible by preemptively putting thoses parentheses.
| | * | Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Gravatar Pierre-Marie Pédrot2016-03-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation.
| | * | Fix #4607: do not read native code files if native compiler was disabled.Gravatar Maxime Dénès2016-03-04
| | | |
| | * | This fix is probably not enough to justify that there are no problems withGravatar Maxime Dénès2016-03-04
| | | | | | | | | | | | | | | | | | | | primitive projections and prop. ext. or univalence, but at least it prevents known proofs of false (see discussion on #4588).
| * | | Adding some standard arguments in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is not perfect and repeats what we do in Pcoq, but it is hard to factorize because rules defined in Pcoq do not have the same precedence. For instance, constr as a Tactic Notation argument is a Pcoq.Constr.constr while as a quotation argument is a Pcoq.Constr.lconstr. We should think of a fix in the long run, but for now it is reasonable to duplicate code.
| | * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
| | | | | | | | | | | | | | | | Fixes compilation of Coq with OCaml 4.03 beta 1.
| * | | All arguments defined through ARGUMENT EXTEND declare a tactic scope.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | | | | | | | | | | | Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now.
| * | | Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Gravatar Pierre-Marie Pédrot2016-03-04
| | | |
| * | | Exchanging roles of tactic_arg and tactic_top_or_arg entries.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | | | | | | | | | | | | | | | The tactic_arg entry was essentially a hack to keep parsing constrs as tactic arguments. We rather use tactic_top_or_arg as the true entry for tactic arguments now.
| * | | Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | | | | | | | | | | | This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there.
| * | | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
| | | |
| * | | Uniformizing the parsing of argument scopes in Ltac.Gravatar Pierre-Marie Pédrot2016-03-04
|/ / /
* | | Merge pull request #97 from clarus/trunkGravatar Pierre-Marie Pédrot2016-03-04
|\ \ \ | | | | | | | | Converting the README to MarkDown syntax.
| | * | Fix a typo in dev/doc/changes.txtGravatar Jason Gross2016-03-04
| | | | | | | | | | | | CQQ -> COQ
| | * | Adding a test for the behaviour of open_constr described in #3777.Gravatar Pierre-Marie Pédrot2016-03-03
| | | |
| | * | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Gravatar Pierre-Marie Pédrot2016-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash.
* | | | Merge branch 'clean-atomic-tactics'Gravatar Pierre-Marie Pédrot2016-02-29
|\ \ \ \
| * | | | Moving the "move" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "exists" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "symmetry" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "generalize dependent" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "clearbody" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "clear" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "cofix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
| | | | |
| * | | | Moving the "fix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
|/ / / /
* | | | Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env.
* | | | Slightly contracting code of evarconv.ml.Gravatar Hugo Herbelin2016-02-28
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:29:12 +0000