aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
their type annotation.
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time.
2015-11-10Updating test-suite after Bracketing Last Introduction Pattern set byHugo Herbelin
default. Interestingly, there is an example where it makes the rest of the proof less natural. Goal forall x y:Z, ... intros [y|p1[|p2|p2]|p1[|p2|p2]]. where case analysis on y is not only in the 2nd and 3rd case, is not anymore easy to do. Still, I find the bracketing of intro-patterns a natural property, and its generalization in all situations a natural expectation for uniformity. So, what to do? The following is e.g. not as compact and "one-shot": intros [|p1|p1]; [intros y|intros [|p2|p2] ..].
2015-11-10Updating Compat85.v after bd1c97653 on bracketing last or-andHugo Herbelin
introduction pattern by default.
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0. Very sorry not ready.
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
the return clause and of the branches in a "match", computing them automatically when using the "at" clause of pattern, destruct, ... In principle, this is a source of incompatibilities in the numbering, since the internal binders of a "match" are now skipped. We shall deal with that later on.
2015-11-10Listing separately changes from 8.5betas to final 8.5 and furtherHugo Herbelin
changes from final 8.5 to next version.
2015-11-10Activating bracketing of last or-and introduction pattern by defaultHugo Herbelin
for more regularity.
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
Did some manual merge in tactics/tactics.ml.
2015-11-10Dead code from the commit having introduced primitive projections (a4043608).Hugo Herbelin
2015-11-10Typo.Hugo Herbelin
2015-11-10Fixing a bug in reporting ill-formed constructor.Hugo Herbelin
For instance, Inductive a (x:=1) := C : a -> True. was wrongly reporting Error: The type of constructor C is not valid; its conclusion must be "a" applied to its parameter. Also "simplifying" explain_ind_err.
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-10Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Pierre-Marie Pédrot
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-11-08Adapting output test inference.v after c23f0cab6 (experimentingHugo Herbelin
printing the type of the defined term of a LetIn).
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2015-11-07Preventing an unwanted warning 5 "this function application is partial"Hugo Herbelin
which e.g. OCaml 4.02.1 displays.
2015-11-07Implementing assert and cut with LetIn rather than using a beta-redex.Hugo Herbelin
Hopefully, it will provide with nicer proof terms, in combination with the commit printing the type of LetIn when the defined term is a proof.
2015-11-07Experimenting printing the type of the defined term of a LetIn whenHugo Herbelin
this type is a proposition. This is based on the assumption that in Prop, what matters first is the statement.
2015-11-07Adding an amazing property of Prop.Hugo Herbelin
2015-11-07Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Hugo Herbelin
For pose/set/clearbody, I think it is clear that we want to preserve the name and this commit do it. For revert, I first did not preserve the name, then considered in 2ba2ca96be88 that it was better to preserve it. For intro, like for revert actually, I did not preserve the name, based on the idea that the type was changing (*). For instance if we have ?f:nat->nat, do we really want to keep the name f in ?f:nat after an intro. For revert, I changed my mind based on the idea that if we had a better control of the name if we keep the name that if the system invents a new one based on the type. I think this is more reasonable than (*), so this commit preserves the name for intro. For generalize, it is still not done because of generalize being in the old proof engine.
2015-11-07Tests for syntax "Show id" and [id]:tac (shelved or not).Hugo Herbelin
2015-11-07Fixing documention of Add Printing Coercion.Hugo Herbelin
2015-11-07Merge remote-tracking branch 'origin/v8.5' into upstream-trunkHugo Herbelin
- Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml
2015-11-06Fixed #4407.Pierre Courtieu
Like coqc: detect if the current directory was set by options, if not: add it with empty logical path. TODO: check if coq_makefile is still correct wrt to this modification, I think yes, actually it should end being more correct.
2015-11-06Fixing #4406 coqdep: No recursive search of ml (-I).Pierre Courtieu
2015-11-06Fixing complexity file f_equal.v.Hugo Herbelin
2015-11-06More on how to compile doc.Hugo Herbelin
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise.
2015-11-05Add test-suite file for #4273.Matthieu Sozeau
2015-11-05Fix bug #4273Matthieu Sozeau
Syntactic analysis of dependencies when atomizing arguments in destruct was not dealing properly with primitive projections hiding their parameters.
2015-11-05Update version numbers and magic numbers for 8.5beta3 release.Maxime Dénès
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Checker was forgetting to register global universes introduced by opaqueMatthieu Sozeau
proofs.
2015-11-04Univs: missing checks in evarsolve with candidates and missing aMatthieu Sozeau
whd_evar in refresh_universes.
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
inconsistent).
2015-11-04Univs: compatibility with 8.4.Matthieu Sozeau
When refreshing a type variable, always use a rigid universe to force the most general universe constraint, as in 8.4.
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
is buggy in general.
2015-11-04Test file for #4397.Maxime Dénès
2015-11-03Update compatibility file for some of bug #4392Jason Gross
Now doing ```coq Tactic Notation "left" "~" := left. Tactic Notation "left" "*" := left. ``` will no longer break the `left` tactic in Coq 8.4. List obtained via ``` grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g' ```
2015-11-02Fix bug #4397: refreshing types in abstract_generalize.Matthieu Sozeau
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-11-02Refresh rigid universes as well, and in 8.4 compatibility mode,Matthieu Sozeau
make them rigid to disallow minimization.
2015-11-02Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Maxime Dénès
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-11-02Made that the syntax [id]:tac also applies to the shelve, which is after all ↵Hugo Herbelin
its main interest!
2015-11-02STM: fix undo into a branch containing side effectsEnrico Tassi
The "master" label used to be reset to the wrong id
2015-11-02STM: never reopen a branch containing side effectsEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 22:31:00 +0000