aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-12-19Fixed some printing details for dependent evars in emacs mode. Patchcourtieu
from Hendrik Tews: 1) Print the dependent evars after "No more subgoals" and after "No more subgoals but non-instantiated existential". This is necessary to correctly display the instantiation status of dependent evars, because the last proof command might change them. 2) Change the ``Show Goal "id"'' command to include a header like goal / evar 2 is: This is more consistent with the other Show commands. Moreover it simplifies the use of this command in Proof General, because, with the change, the output contains the goal ID. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14824 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
unfolded fixpoints when calling destruct). However, this might break compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18CoqIde files position is freedesktop compliant.pboutill
Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18./configure & freedesktoppboutill
1/ man dir is now prefix/share/man and not prefix/man git diff! 2/ a data dir option for coqide extra data. 3/ typo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
interpretation order of scoped notations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14819 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Applied patches proposed suggested by Hendrik Tews to fix existentialcourtieu
variables printing in emacs mode (put them at the end of input, and fix commas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14818 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Continuing 14812 and 14813 (use type information to reduce theherbelin
applicability of first-order unification in tactic unification). Don't try to unify the type (this would require a unification power that unification.ml does not have - and some contribs complain about that). Just reject first-order unification of metavariables of higher-order types when their types are obviously incompatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14817 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Removing PrintConstr debugging entry in g_proof.ml4 which was notherbelin
working and was causing a warning when declaring the entry of same name in top_printers.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14815 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Suspending declaration of undefined debug printers.herbelin
(Matthieu, do you have a definition for these printers around?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14814 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
meta in the tactic unification algorithm ("auto" becomes much slower if it takes into account the type of metas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14813 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Added ability to take the type of applied metas into account whenherbelin
instantiating them in the unification algorithm used for tactics. This allows to discard ill-typed uses of first-order unification which otherwise would have been fatal (this incidentally allows to partially restore some compatibility with 8.3 that was broken after eta was added in unification). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Reorganizing Unification.unify_0 so as to more easily share codeherbelin
between branches. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14811 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Coq_makefile: "beautify" targetpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14809 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Coqdep adds %.v.beautified on the left of the ':' when it generates %.v ↵pboutill
dependecies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14808 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Coq_makefile: "validate" target calls the checker over all vo.pboutill
It uses short names so clashes can occur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14807 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Coq_makefile: section refactoring and no variables for OCaml if no ml* files ↵pboutill
in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14806 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Coq_makefile: if no -install is provided, install location is set by a ↵pboutill
Makefile variable or a special target. 1/ defining the USERINSTALL variable make a "user" installation instead of a "global" one. 2/ make userinstall is an alias for make USERINSTALL=true install git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14805 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Deactivated automatic inference of _case schemes, as it was in 8.3herbelin
(mainly to avoid defining names that may clash with user names later on). Best approach will probably be to define inductive types in relevant "name spaces". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14804 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
as to ensure the warning is flushed in real time. Made systematic the use of if_warn instead of if_verbose when the warning is intended to signal something anormal (if_warn is activated when compiling verbosely and when working interactively while if_verbose is activated only when working interactively and when loading verbosely). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Bypassing the use of (currently unimplemented) "Show Script" in testsherbelin
that used it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14802 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Improving pretty-printing of Ltac functions.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14801 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Fixing format of complexity bug Notations.v.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14800 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Fixing previous commit which was bugging on tactics preceded by goal number ↵courtieu
(2:intros.). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14799 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Coqide: adapt some comments now that bullets are terminators like { }letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14798 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
known in advance to be instantiable by only a finite number of terms. When an evar with candidates remain unsolved after unification, the first candidate is taken as a heuristic. This is used in particular to reduce the number of pending conversion problems when trying to infer the return clause of a pattern-matching problem. As an example, this repairs test 2615.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14797 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Fixing amazing loop when using eta-expansion in pattern-matching forherbelin
printing notations. Since notation printing is not typed, printing "F G" using a notation for "f (fun x => g)" recursively eta-expands G, then x, then a new x and so on forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Adapting coqide to my last commit: courtieu
Moving bullets (-, +, *) into stand-alone commands instead of being part of a tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14795 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
part of a tactic. WARNING: Coqide needs to be adapted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14794 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries ↵ppedrot
: goal description, with focused and unfocused goals, and list of currently declared evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14793 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-14Some extra universe refreshing seems needed in abstract_generalizeherbelin
(for generalize_eqs). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14792 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-12CHANGES: some more updatesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14791 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-12Proof using ...gareuselesinge
New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-10Extraction: only do the test on generalizable lets for ocamlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14785 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-08Makefile: force the installation of all .cmi (and remove some obsolete .mli)letouzey
The previous code wasn't detecting and installing .cmi coming from .mli without corresponding .ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14783 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-08Extraction: avoid internal eta-reduction (fix #2570)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14782 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
(the number of entries to reset was not correct). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14778 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14777 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
is imported): in case of nested modules, activation was done as soon as the outermost module was imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14775 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Html page titlespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Vectors use a bit more the pattern matching compilerpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14773 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Typopboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14772 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Fixed a synchronization bug between coqtop and the CoqIDE command pane.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14771 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06fix Makefile.common handling of -byte-onlygareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14770 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation of Arguments + implicitsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation for Arguments + notation scopesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14768 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation for Arguments + simplgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14767 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Minor fixes to Argumentsgareuselesinge
- Implicit arguments can be mentioned anonymously: Arguments map {_ _} f l. - To rename implicit arguments, the ": rename" flag must be used: Arguments map {T1 T2} f l : rename. Without the ": rename" flag arguments can be used to assert that a function has indeed the expected number of arguments and that the arguments are named as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Backtrack on synchronizing universe counter with resetherbelin
mechanism, section discharge is not ready for that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14765 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 10:23:10 +0000