aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Add a test-suite file ensuring coinductives with primitive projectionsGravatar Matthieu Sozeau2015-03-03
| | | | | do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching.
* Fix test-suite file, this is currently a wontfix, but keep theGravatar Matthieu Sozeau2015-03-03
| | | | test-suite file for when we move to a better implementation.
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
| | | | | | pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches.
* Improving display of camlp4/camlp5 versions, library and binary locations.Gravatar Hugo Herbelin2015-03-03
|
* Reinstalling search of camlpX in camldir, when given, forGravatar Hugo Herbelin2015-03-03
| | | | | | | compatibility with pre-1b7d4a033af heuristic in searching camlpX (continuation of a joint patch with Maxime). Typo basename -> dirname.
* Typos in doc modules.Gravatar Hugo Herbelin2015-03-03
|
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
| | | | cases, in some cases.
* Fix bug #4101, noccur_evar's expand_projection can legitimately failGravatar Matthieu Sozeau2015-03-03
| | | | when called from w_unify, so we protect it.
* Fix bug introduced by my last commit, forgetting to adjust de BruijnGravatar Matthieu Sozeau2015-03-03
| | | | index lookup.
* Fix bug #4097.Gravatar Matthieu Sozeau2015-03-02
|
* Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
|
* Coq_makefile clean target erases .coq-native dirs in . if they are emptyGravatar Pierre Boutillier2015-02-28
|
* Fixing the rule for ml4 depencies in coq_makefileGravatar mlasson2015-02-28
|
* Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ↵Gravatar Pierre Boutillier2015-02-28
| | | | r15439 as we were talking at that time)
* Adding a test for bug #3612.Gravatar Pierre-Marie Pédrot2015-02-27
|
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
|
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-27
|
* Test for bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
|
* Fixing bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
| | | | | | | Instead of substituting carelessly the recursive names in Ltac interpretation, we declare them in the environment beforehand, so that they get globalized as themselves. We restore the environment afterwards by transactifying the globalization procedure.
* Taking current env and not global env in b286c9f4f42f (4 commits ago,Gravatar Hugo Herbelin2015-02-27
| | | | as revealed by #2141).
* simpl: honor Global for "simpl: never" (Close: 3206)Gravatar Enrico Tassi2015-02-27
| | | | It was an integer overflow! All sorts of memories.
* STM: Considering Stack_overflow as a normal tactic error (Close #3576)Gravatar Enrico Tassi2015-02-27
|
* Fix test for #3467, I had moved it in a dumb way.Gravatar Maxime Dénès2015-02-27
|
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
| | | | | | | | | is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
* Hack so that refine_no_check accepts an argument which is a match on anGravatar Hugo Herbelin2015-02-27
| | | | inductive type with let-in in the arity (until logic.ml disappears).
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
| | | | clause in the presence of let-ins in the arity of inductive type).
* Fixing typo resulting in wrong printing of return clauses forGravatar Hugo Herbelin2015-02-27
| | | | inductive types with let-in in arity.
* Fix test for #3848, still open.Gravatar Maxime Dénès2015-02-27
|
* Moving test for #3467 to closed after PMP's fix.Gravatar Maxime Dénès2015-02-27
|
* Fix test-suite files for bugs #2456 and #3593, still open.Gravatar Maxime Dénès2015-02-27
|
* Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵Gravatar Guillaume Melquiond2015-02-27
| | | | bug #4080)
* Somehow fixing bug #3467.Gravatar Pierre-Marie Pédrot2015-02-27
| | | | | | The notations using tactics in term seem now not to respect globalized names. It is not obvious that this is the expected behaviour, but at least it does not die with an anomaly.
* Add test-suite file for #3649.Gravatar Maxime Dénès2015-02-27
|
* Moving tests for #2456 and #3593 to "opened" until they're fixed.Gravatar Maxime Dénès2015-02-27
|
* Made test for #3392 rely less on unification.Gravatar Maxime Dénès2015-02-27
|
* Moving test of #3848 to "opened".Gravatar Maxime Dénès2015-02-27
|
* Test for #2602, which seems now fixed.Gravatar Maxime Dénès2015-02-26
|
* Test for bug #3298.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Fixing bug #3298.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Trying to fix code locating camlp4/camlp5.Gravatar Maxime Dénès2015-02-26
| | | | Should fix #3396 and #3964.
* Fixing bug 3099.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Fixing printing error in coq_makefile.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Fixing printing of ordinals.Gravatar Pierre-Marie Pédrot2015-02-26
|
* Mention -R option in warnings, fixing #4067 and #4068.Gravatar Maxime Dénès2015-02-26
|
* Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
|
* Fixing complexity tests for #4076.Gravatar Maxime Dénès2015-02-26
|
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
| | | | | | | | | This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035.
* Moving test for bug #3681 as closed.Gravatar Pierre-Marie Pédrot2015-02-26
|
* CoqIDE: correclty unfocus (remove all tags) when jumping out of a proofGravatar Enrico Tassi2015-02-25
|
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
| | | | | Workers send back incomplete system states (only the proof part). Such part must include the meta/evar counter.
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-06 03:41:57 +0000