| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
ie default goal selector !
How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
[C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
until there are no errors (NB the first [C-c f] has no effect).
You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
my/bullet-stack (6 layers is enough the vast majority of the time
though). The system will give you an error and you need to finish
the lemma manually.
- weird indentation when a bullet starts in the middle of a line and
doesn't end in that line. Just reindent as you like then go to the
next error and continue.
~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
"Which bullets should be used, in order.")
(defvar-local my/bullet-count nil
"The value in the car indicates how many goals remain in the
bullet at (length-1), and so on recursively. nil means we
haven't started bulleting the current proof.")
(defvar-local my/last-seen-qed nil)
(defun my/get-maybe-bullet-error ()
"Extract the number of focused goals from the ! selector error message."
(when-let* ((rbuf (get-buffer "*response*"))
(str (with-current-buffer "*response*" (buffer-string)))
(_ (string-match
(rx "Error: Expected a single focused goal but " (group (+ digit)))
str))
(ngoals (string-to-number (match-string 1 str))))
ngoals))
(defun my/bullet-fix-indent ()
"Auto indent until the next Qed/Defined, and update my/last-seen-qed."
;; (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
(when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
(set-marker my/last-seen-qed qed)
(indent-region (- (point) 1) qed)))
(defun my/nth-bullet (n)
"Get nth bullet, erroring if n >= length my/bullet-stack"
(or (nth n my/bullet-stack)
(error "Too many bullets.")))
(defun my/maybe-fix-bullet-error (&optional arg)
"Main function for porting a file to strict focusing.
Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.
Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.
This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
(interactive "P")
(unless my/last-seen-qed
(setq my/last-seen-qed (set-marker (make-marker) 0)))
(when (or arg (> (point) my/last-seen-qed))
(setq my/bullet-count nil)
(set-marker my/last-seen-qed 0))
(when-let ((ngoals (my/get-maybe-bullet-error)))
(setq my/prev-count (format "%s %s" ngoals my/bullet-count))
(if (= ngoals 0)
(progn
(while (and my/bullet-count (= (car my/bullet-count) 0))
(pop my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
(my/bullet-fix-indent))
(setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(my/bullet-fix-indent))))
(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~
|
|
|
|
|
|
|
|
|
|
|
|
|
|
induction/elim over a dependent elimination principle for Prop
arguments.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
add_definition/fixpoint and parsing of the "Program" prefix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
doc is ok). Rework the .v files in Program accordingly, adding some
documentation and proper headers. Integrate the development of an
elimination principle for measured functions in Program/Wf by Eelis van
der Weegen.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fix a typo in lowercase_utf8
- Fix generation of signatures in subtac_cases not working for dependent
inductive types with dependent indices.
- Fix coercion of inductive types generating ill-typed terms.
- Fix test script using new syntax for Instances.
- Move simpl_existTs to Program.Equality and use it in simpl_depind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binders.
- Change syntax of type class instances to better match the usual syntax of
lemmas/definitions with name first, then arguments ":" instance.
Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
Program.Utils, and subset_scope as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Allow unicode superscripts characters.
- Put Program notations in scopes.
- Correct priority semantics in typeclasses eauto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
check_required_library where needed (fixes bug #1797).
Remove spurious messages from ring when not in verbose mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
document it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
