aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-09-01create_session takes the filename as argument.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14437 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01No more parser for reading coqide pref filepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14436 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01[/]+ is equivalent to [/] in System and its copypboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14435 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile.absolute_dir -> Minilib.canonical_path_namepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14434 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Creation of ide/project_file.ml4pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01gitignore updatepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14432 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: Bug fix of check_deppboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14431 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: process_cmd_line is purely functional.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14430 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: No other function than split_arguments uses a target type.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14429 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: New option -arg to specify a compiler option.pboutill
Consequently, option -impredicative-set is deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14428 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile drops the '/' at the end of physical path of -I and -Rpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14427 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Several bug reports came from confusions between generalize and set.pboutill
Maybe, people will read the two sections of the ref-man at the same time if they are one after the other... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14426 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Bug 2583: Update of the syntax of terms in the reference manualpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14425 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Bug 2577: Second attempt to be correct.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14424 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-30Porting Hendrik's 8.3 patch for proof tree visualization under proofherbelin
general to trunk (only printing of goal ID done - printing of instantiated dependent evars not done). (joint work with Arnaud) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14423 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-30Quick improvement of some error messages related to module applicationherbelin
(localization of the error and hopefully improved messages) [Is there a reason why the restriction is not enforced at the parsing level? Anyway, treating it at interpretation time allows more appropriate messages] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14422 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-25Extraction: allow extraction of records with anonymous fields (fix #2555)letouzey
For Ocaml, we now use the extraction-reserved substring "__" : The name foo__i will be pick for i-th field of record foo if it is anonymous. For Haskell, still no printing of records as native records, hence nothing to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-23Use of the standard terminology for Diaconescu's theorem (not "paradox").herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14419 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-23Clarifying that only identifiers are advertised to be turned into keywordsherbelin
(or shall we advertise also non-ident keywords?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14418 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-22Tactics.compute_scheme_signature: factorize the two almost-similar casesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14417 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-18Updates in CHANGESletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14416 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-18Remove old file (1999)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14415 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-18Misc improvements concerning "Show Match" and its coqide equivalentletouzey
- The make_cases function was duplicated in two files - Rather use next_name_away_in_cases_pattern instead of ..._in_goal when finding fresh pattern variables - Nicer final pretty-print via some formatting boxes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14414 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-17Give inner fixpoint of gcd31 a name, to avoid excessive unfoldingglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14413 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-17Smaller proof terms for QcPower_{0,pos}glondu
The use of compute produces huge terms that contain hundreds of unfolded Zadd, Zmul, Zsucc! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14412 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-16Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14411 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-13New fix for is_ident_not_keyword.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14410 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-12Fixes mini-bug: Qed would succeed even on focused proofs.aspiwack
It allowed proofs of the Shape [{ solve. Qed.] which is inelegant at best. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14409 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
Instead of hard-coding in search.ml some substrings such as "_admitted" or "_subproof" we don't want to see in results of SearchAbout and co, we now have a user command: Add Search Blacklist "foo". Remove Search Blacklist "foo". (* the opposite *) Print Table Search Blacklist. (* the current state *) In Prelude.v, three substrings are blacklisted originally: - "_admitted" for internal lemmas due to admit. - "_subproof" for internal lemmas due to abstract. - "Private_" for hiding auxiliary modules not meant for global usage. Note that substrings are searched in the fully qualified names of the available lemmas (e.g. "Coq.Init.Peano.plus"). This commit also adds the prefix "Private_" to some internal modules in Numbers, Z, N, etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14408 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Fixing typos in commentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14406 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Improving error message about coinductive guard (old "cases" is now "match")herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14405 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Fixing printing bug with last trailing non-maximally implicitherbelin
arguments needed for correct typing of partial applications (knowing that in practice, users should anyway better declare such arguments as maximally inserted). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14404 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Exported tactic intro_thenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14403 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Made CHANGES more uniformly writtenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14402 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Take benefit of bullets available by default in Preludeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14401 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
"rewrite Heq in H" but "rewrite" is sometimes used by users and I don't want to have to change their file. The solution to put the notations in a module does not work with name "rewrite" because loading the module would change the status of "rewrite" from simple ident to keyword (and we cannot declare "rewrite" as an ident, as shown in previous commit). Then we come back on notation "rew" (this name is also used by some users), in a module. This continues commit r14366 and r14390 and improves on the level of the notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14400 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
(it does not work) Indeed, if a rule in operconstr at some level starts with an ident, it has to be declared as a keyword because other rules whose leftmost call is a call to operconstr will eventually the top level "200" even thought this leftmost operconstr might be declared at a lower level. This is for instance the reason why "True /\ forall x, x=0" is parsed even though /\ expects arguments at level less than 80 and forall is at level 200. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14399 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Fix implementation of Hint Immediate used by typeclasses eautomsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14398 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Added list_map_filter_imsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14397 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Graceful error message for [Proof Mode] and [Set Default Proof Mode] when ↵aspiwack
requiring a non-existing proof mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14396 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-09BinInt: more structured scripts thanks to bullets and { }letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14395 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-09Coqide: revised parsing of coq sentencesletouzey
In particular, grouping { and } delimiters is now allowed. The only place where blank (i.e. space or newline or eof) is mandatory is after dots. For instance "{{tac. }{tac. }}" is ok, while "tac.}" is not seen as containing any sentence delimiter but rather the inner-sentence token ".}", that might have been registered (or not) to Coq by the user via some tactic or constr notation. This way, coqide should be in sync with what is accepted by coqtop. Current cvs version of proofgeneral is slightly more laxist, but this will probably be harmonized soon. Technically, we cannot rely anymore on functions like forward_to_tag_toggle, since two delimiters "}}" could be adjacent, hence no toogle of the corresponding tag. Instead, we use a simplier (less efficient ?) iterative search. When retagging a zone after some edition, we retag up to a real "." delimiter (or eof), since the status of "{" "}" as delimiters is too fragile to be trusted after edition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14394 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-09In coqtop, a terminating "." must now be followed by a blank or eof.letouzey
This way, we forbid contiguous sentences like "tac.{tac.}", which should now be written with at least 2 spaces: "tac. {tac. }" This should avoid confusion if a user declare a notation involving ".{" or ".}" as tokens. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14393 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-09Moved the declaration of "Classic" being the default proof mode to coqtop.ml ↵aspiwack
so that the files in Init can benefit from the full-blown tactic language. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14392 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Some forgotten lemma in Arith with "O" in the name instead of "0".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14391 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
a smaller risk that "rewrite" clashes with a name used for constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14390 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
(an articulating ident needs to be a keyword if the constr entry that preceeds it is higher than the level of applications). Also fixed is_ident_not_keyword which only looked at the first letter and at the keyword status to decide if a token is an ident. This allowed to simplified define_keywords in Metasyntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14389 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Two bugs in pattern-matching compilation:herbelin
- when several variables are generalized in a row (in compile_alias) - with constructors having more than one argument in some inductive family when the dependencies are used in the predicate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14388 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Term: fix hash_constr to hash modulo casts & names (like compare_constr)puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14387 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:22:19 +0000