aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - Allow parsing of @const@{instance} for specifying universe instances of ↵Gravatar Matthieu Sozeau2014-06-04
| | | | | | polymorphic constants.
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
| | | | - Finish the change to level-to-level substitutions, in the checker.
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
| | | | | | | - Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level substitutions where the more general level-to-universe substitutions were previously used.
* Fix handling of anonymous Type in template universe polymorphic inductivesGravatar Matthieu Sozeau2014-06-04
| | | | to not interfere with already declared universes.
* - Keep all <= constraints during refinement, otherwise we might miss ↵Gravatar Matthieu Sozeau2014-06-04
| | | | | | | collapsed universes. - Fix normalization with universe substitutions during refinement being inconsistent with the one in the kernel.
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
| | | | | Of course, this is an under approximation of the expected behavior : unfolding a constant iff a leaf of its underlying split-tree is reached.
* A bug has been closed (HoTT/coq #105)Gravatar Jason Gross2014-06-03
|
* The tactic interpreter now uses a new type of tactics, throughGravatar Pierre-Marie Pédrot2014-06-03
| | | | | | | | | | | the GTac module. A ['a Gtac.t] is a special case of tactic that may depend on the current goals, or not. Internally, it construct a list of results, one for each focussed goal, if the tactic is actually dependent. This allows for an interpretation of whole-goal tactic that does work, which was not the case for the previous implementation, which did to many Proofview.Goal.enter.
* Fixing incorrect printf format.Gravatar Pierre-Marie Pédrot2014-06-02
|
* Removing symmetry from the atomic tactics.Gravatar Pierre-Marie Pédrot2014-06-02
|
* A little bit of documentation about V5.10 and V6.3 and V7.Gravatar Hugo Herbelin2014-06-01
|
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | destruction of schemes in Type such as sumbool. Added an option "Set Standard Proposition Elimination Names" for governing this strategy (activated by default). This provides names supposingly more uniform than before for those who like to have names automatically generated, at least in the first phase of the development process of proofs. Examples: *** Non dependent case *** Goal {True}+{False}-> True. intros [|]. Before: t : True ============================ True and f : False ============================ True After: H : True ============================ True H : False ============================ True *** Dependent case *** Goal forall x:{True}+{False}, x=x. intros [|]. Before: t : True ============================ left t = left t f : False ============================ right f = right f After: HTrue : True ============================ left HTrue = left HTrue HFalse : False ============================ right HFalse = right HFalse
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
| | | | | | | | | in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop.
* More on injection over a projectable "existT". - Fixing syntax "injection ↵Gravatar Hugo Herbelin2014-05-31
| | | | ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).
* Fixing introduction patterns * and ** when used in a branch so that they do ↵Gravatar Hugo Herbelin2014-05-31
| | | | not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
|
* Basic lemmas about the algebraic structure of equality.Gravatar Hugo Herbelin2014-05-31
|
* Dead code + typo.Gravatar Hugo Herbelin2014-05-31
|
* Adding test-suite for bug #3355.Gravatar Pierre-Marie Pédrot2014-05-30
|
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
| | | | | | cases of Type (* Prop *) <= Set. - Do check types of metavariables at the end of apply's unification, if it failed at the beginning (otherwise universe constraints can be incomplete).
* Removing a tclSENSITIVE from rewrite.Gravatar Pierre-Marie Pédrot2014-05-27
|
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
| | | | (refolding of cbn is smarter)
* Reduction.Stack.Fix/Case stores Cst_stack.tGravatar Pierre Boutillier2014-05-26
|
* Cst_stack before stack (abstraction leak in whd_gen)Gravatar Pierre Boutillier2014-05-26
|
* cbn: args list instead of arg numberGravatar Pierre Boutillier2014-05-26
|
* Reductionops.Stack.map & Reduction.iterate_whd_genGravatar Pierre2014-05-26
|
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
| | | | | | | | | correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes.
* Update infer_conv to record trivial Prop <= Type i constraints that are ↵Gravatar Matthieu Sozeau2014-05-26
| | | | | | needed during unification.
* make coqdep canonicalize paths from the command lineGravatar Gregory Malecha2014-05-26
| | | | | | | | - logical paths given to -R and -I should be split on periods. - it also seems like giving an empty string should result in the empty path rather than the singleton path with an empty string as an identifier.
* Fixing commit 9cef834. The parsing rules were generating an empty list,Gravatar Pierre-Marie Pédrot2014-05-26
| | | | conflicting with the previous behaviour of 'eexists'.
* Revert "Chasing the goal entering backward while interpreting tactics. This ↵Gravatar Pierre-Marie Pédrot2014-05-24
| | | | | | | | required" I tested the commit on the wrong branch... This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
* Chasing the goal entering backward while interpreting tactics. This requiredGravatar Pierre-Marie Pédrot2014-05-24
| | | | | writing a new primitive recovering the first goal under focus. It sounds a bit hackish, but it does actually work.
* Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholeGravatar Pierre-Marie Pédrot2014-05-24
| | | | | | | | proof. Indeed, computing an empty list of arguments triggered a Proofview.Goal.enter, which broke tactics like [shelve_unifiable]. This does not fix this particular tactic though, because the Ltac interpreter still enters the goal when calling a Ltac reference.
* Complying with reference manual for the syntax of exists/eexists, i.e.Gravatar Hugo Herbelin2014-05-24
| | | | | | | | | | | removing the strange kind of syntax "exists ,t,". which was equivalent to "split; exists t; split", as in e.g.: Goal (exists x, x=0) /\ (exists x, x=0). exists ,0,. Qed. This answers bug request #3340.
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
| | | | variant of it, accepting an additional integer.
* Fix native_compute for systems with a limited size for the command line.Gravatar Guillaume Melquiond2014-05-22
| | | | | | | | | | | | | | The call to the native compiler can fail due to the sheer amounts of -I options passed to it. Indeed, it is easy to get the command line to exceed 512KB, thus causing various operating systems to reject it. This commit avoids the issue by only passing the -I options that matter for the currently compiled code. Note that, in the worst case, this commit is still not sufficient on Windows (32KB max), but this worst case should be rather uncommon and thus can be ignored for now. For the record, the command-line size mandated by Posix is 4KB.
* Ignore generated file.Gravatar Guillaume Melquiond2014-05-22
|
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
|
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
|
* Allowing Ltac definitions that may be unusable because of a built-inGravatar Pierre-Marie Pédrot2014-05-21
| | | | parsing rule.
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
|
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
|
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
| | | | | | | | | "foobar" constr(x1) ... constr(xn) are now defined as pure Ltac definitions, and do not add grammar nor printing rules. This partially relies on a hack consisting in retrieving the arguments in the tactic environment rather than as directly passed to the TacExtend node.
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
| | | | | | | | We eta-expand primitive Ltac functions, and instead of feeding TacExtend directly with its arguments, we use the environment to retrieve them. Some tactics from the AST were also moved away and made using this mechanism.
* Revert "Fix Qcanon after changes on injection."Gravatar Maxime Dénès2014-05-18
| | | | This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e.
* When discrimination is not possible, try to project.Gravatar Maxime Dénès2014-05-18
| | | | | | | | | | | | Example: Inductive Pnat : Prop := O | S : Pnat -> Pnat. Variable m n : Pnat. Goal S (S O) = S O -> False. intros H; injection H. now deduces S O = O instead of failing with an error message.
* Suggest Set Injection On Proofs in error message for injection.Gravatar Maxime Dénès2014-05-18
|
* Restored old behavior of injection on proofs by default.Gravatar Maxime Dénès2014-05-18
| | | | Use Set Injection On Proof to enable the new behavior.
* Adding way to get the list of the accepted tactic notation arguments.Gravatar Pierre-Marie Pédrot2014-05-17
|
* Fixing coqdep_boot warning relative to unknown ML files that were in tactics.Gravatar Pierre-Marie Pédrot2014-05-17
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-04 03:56:59 +0000