aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* New fix for is_ident_not_keyword.Gravatar herbelin2011-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes mini-bug: Qed would succeed even on focused proofs.Gravatar aspiwack2011-08-12
| | | | | | 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
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
| | | | | | | | | | | | | | | | | | | | | | | | 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
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Fixing typos in commentsGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving error message about coinductive guard (old "cases" is now "match")Gravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing printing bug with last trailing non-maximally implicitGravatar herbelin2011-08-10
| | | | | | | | 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
* Exported tactic intro_thenGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made CHANGES more uniformly writtenGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of bullets available by default in PreludeGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | "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
* Partly revert commit r14389 about relaxing the condition for being a keywordGravatar herbelin2011-08-10
| | | | | | | | | | | | | | (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
* Fix implementation of Hint Immediate used by typeclasses eautoGravatar msozeau2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added list_map_filter_iGravatar msozeau2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Graceful error message for [Proof Mode] and [Set Default Proof Mode] when ↵Gravatar aspiwack2011-08-10
| | | | | | requiring a non-existing proof mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14396 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinInt: more structured scripts thanks to bullets and { }Gravatar letouzey2011-08-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: revised parsing of coq sentencesGravatar letouzey2011-08-09
| | | | | | | | | | | | | | | | | | | | | | | | 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
* In coqtop, a terminating "." must now be followed by a blank or eof.Gravatar letouzey2011-08-09
| | | | | | | | | | 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
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ↵Gravatar aspiwack2011-08-09
| | | | | | 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
* Some forgotten lemma in Arith with "O" in the name instead of "0".Gravatar herbelin2011-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14391 85f007b7-540e-0410-9357-904b9bb8a0f7
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
| | | | | | 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
* Be a bit less aggressive in declaring idents as keywords in notationsGravatar herbelin2011-08-08
| | | | | | | | | | | (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
* Two bugs in pattern-matching compilation:Gravatar herbelin2011-08-08
| | | | | | | | - 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
* Term: fix hash_constr to hash modulo casts & names (like compare_constr)Gravatar puech2011-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
| | | | | | | Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
* moins de reification inutile, noatations standardsGravatar pottier2011-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unification: detect invalid evar instantiations due to scoping earlier.Gravatar msozeau2011-08-04
| | | | | | Add a debug printer for existential sets (used for frozen_evars in w_unify). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix nf_evars_undefined use in pr_constraintsGravatar msozeau2011-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix nf_evars_undefinedGravatar msozeau2011-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch to simplify is_open_canonical_projectionGravatar herbelin2011-08-02
| | | | | | (courtesy from François Garillot) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14381 85f007b7-540e-0410-9357-904b9bb8a0f7
* More robust evar_map debugging printerGravatar herbelin2011-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: simplify compare_constr by removing calls to decompose_appGravatar puech2011-08-01
| | | | | | I think the additional check was here for historical reasons (before the invariant on Apps was enforced) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added .dir-locals file to take advantage of emacs 23's new Directory-local ↵Gravatar puech2011-08-01
| | | | | | | | | | | variables. These variables are set whenever we open a file in the source tree. It sets: * the default directory where to launch compilation (the root directory) * the TAGS file location * the camldebug command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14378 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug 2580. Quick fix: copy emitcodes before patching itGravatar barras2011-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring: replaced various generic = on constr by eq_constr, destructors etc.Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quote: replaced various generic = on constr by eq_constr, destructors etc.Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14374 85f007b7-540e-0410-9357-904b9bb8a0f7
* generic = on named_context replaced by named_context_equalGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Newring: generic = on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_micromega: generic = on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Field: generic Gmap on constr replaced by CmapGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract_env: generic = on prec_declaration replaced by prec_declaration_equalGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tactics: replace generic = on constr by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14368 85f007b7-540e-0410-9357-904b9bb8a0f7
* Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: replace generic = on mutual_inductive_body by mib_equalGravatar puech2011-07-29
| | | | | | Term: add function eq_rel_declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: replace generic list_distinct on constr by constr_list_distinctGravatar puech2011-07-29
| | | | | | This new function is a copy of Util's one, but working on Constrhash git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14365 85f007b7-540e-0410-9357-904b9bb8a0f7
* replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac_cases: replaced some generic = on constr by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring: replaced some generic Pervasives.compare on constr by constr_ordGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add printer dependency to Hashtbl_alt (used in Term)Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nsatz: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14360 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-20 16:24:02 +0000