aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Pretty printing of generalized binderGravatar pboutill2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the pretty-printing of the Program plugin.Gravatar ppedrot2012-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some fix in beautify pretty-printerGravatar pboutill2012-01-17
| | | | | | | | | - In binders, {X} were printed X - Notation toto x y := were printed Notation totox y - Fixpoint declaration prints too much spaces Hunt is not closed yet anyway... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
| | | | | | | - Functions without _env use the global env. - More comments about when letin are counted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix printing of instances, generalized arguments.Gravatar msozeau2012-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some printing details for dependent evars in emacs mode. PatchGravatar courtieu2011-12-19
| | | | | | | | | | | | | | | | 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
* Applied patches proposed suggested by Hendrik Tews to fix existentialGravatar courtieu2011-12-18
| | | | | | | | 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
* Removing PrintConstr debugging entry in g_proof.ml4 which was notGravatar herbelin2011-12-18
| | | | | | | 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
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
| | | | | | | | | | 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
* Improving pretty-printing of Ltac functions.Gravatar herbelin2011-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing previous commit which was bugging on tactics preceded by goal number ↵Gravatar courtieu2011-12-16
| | | | | | (2:intros.). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving bullets (-, +, *) into stand-alone commands instead of beingGravatar courtieu2011-12-16
| | | | | | | | 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
* Proof using ...Gravatar gareuselesinge2011-12-12
| | | | | | | | | | | | | 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
* Makefile: force the installation of all .cmi (and remove some obsolete .mli)Gravatar letouzey2011-12-08
| | | | | | | 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
* Fixing grammar resetting bug in the presence of levels initially emptyGravatar herbelin2011-12-07
| | | | | | (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
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
| | | | | | | | | | | | | | | | - 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
* Fixing superflous newline in output of About when no parameter is renamed.Gravatar herbelin2011-12-04
| | | | | | | | | Fixing output tests after having added flushing of warning in revisions 14747 and 14750. Moving Implicit output test to new command Arguments. Adding test of new Arguments syntax in PrintInfos.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r14747 being actually incomplete (flushing warnings andGravatar herbelin2011-11-30
| | | | | | printing them only if verbose). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Preventing Implicit Arguments warning to be shown in non verbose modeGravatar herbelin2011-11-30
| | | | | | + flushing printing of the message . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14747 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* In emacs mode, prints a list of the dependent existential variables introducedGravatar aspiwack2011-11-23
| | | | | | | | during the proof together with information whether they were (partially) instantiated and if it's the case the list of existential variables that were used to that effect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
| | | | | | | | Example: Arguments eq_refl {B y}, [B] y. Check (eq_refl (B := nat)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
* New Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new vernacular "Arguments" attaches to constants the extra-logical piece of information regarding implicit arguments, notation scopes and the behaviour of the simpl tactic. The About vernacular is extended to print the new extra logical data for simpl. Examples: Arguments foo {A B}%type f [T] x. (* declares A B and T as implicit arguments, A B maximally inserted. declares type_scope on A and B *) Arguments foo {A%type b%nat} p%myscope q. (* declares A and b as maximally inserted implicit arguments. declares type_scope on A, nat_scope on b and the scope delimited by myscope on p *) Arguments foo (A B)%type c d. (* declares A and b in type_scope, but not as implicit arguments. *) Arguments foo A B c. (* leaves implicit arguments and scopes declared for foo untouched *) Arguments foo A B c : clear implicits (* equivalente too Implicit Arguments foo [] *) Arguments foo A B c : clear scopes (* equivalente too Arguments Scope foo [_ _ _] *) Arguments foo A B c : clear scopes, clear implicits Arguments foo A B c : clear implicits, clear scopes Arguments foo A B c : clear scopes and implicits Arguments foo A B c : clear implicits and scopes (* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *) Arguments foo A B c : default implicits. (* equivalent to Implicit Arguments foo. *) Arguments foo {A B} x , A [B] x. (* equivalent to Implicit Arguments foo [[A] [B]] [B]. *) Arguments foo a !b c !d. (* foo is unfolded by simpl if b and d evaluate to a constructor *) Arguments foo a b c / d. (* foo is unfolded by simpl if applied to 3 arguments *) Arguments foo a !b c / d. (* foo is unfolded by simpl if applied to 3 arguments and if b evaluates to a constructor *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the type infrastructure to handle properly API management of optionsGravatar ppedrot2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix parsing of :>> and backtrack correctly on the cache of hints for local ↵Gravatar msozeau2011-11-18
| | | | | | contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a printing function to handle single evarsGravatar ppedrot2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore backward compatibility. ":>" declares subinstances in Class ↵Gravatar msozeau2011-11-18
| | | | | | | | | | declarations, in the usual backward mode, the new token ":>>" declares the subinstance as a forward hint. Both declare a coercion in other contexts. Cleanup the code for declarations for less confusion between coercions and subinstance hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
| | | | | | | | | | | how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
| | | | | | | | | | | | | | This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing beautification of "thm_token" (missing space) + improvements.Gravatar herbelin2011-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For instance, consider this inductive type: Inductive Ind := A | B | C | D. For detecting "match" on this type, one was forced earlier to write code in Ltac using "match goal" and/or "context [...]" and long patterns such as: match _ with A => _ | B => _ | C => _ | D => _ end After this patch, this pattern can be shortened in many alternative ways: match _ with A => _ | _ => _ end match _ with B => _ | _ => _ end match _ in Ind with _ => _ end Indeed, if we want to detect a "match" of a given type, we can either leave at least one branch where a constructor is explicit, or use a "in" annotation. Now, we can also detect any "match" regardless of its type: match _ with _ => _ end Note : this will even detect "match" over empty inductive types. Compatibility should be preserved, since "match _ with end" will continue to correspond only to empty inductive types. Internally, the constr_pattern PCase has changed quite a lot, a few elements are now grouped into a case_info_pattern record, while branches are now lists of given sub-patterns. NB: writing "match" with missing last branches in a constr pattern was actually tolerated by Pattern.pattern_of_glob_constr earlier, since the number of constructor per inductive is unknown there. And this was triggering an uncaught exception in a array_fold_left_2 in Matching later. Oups. At least this patch fixes this issue... Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number of branch in a match pattern. I doubt this was really a problem, but having now linear code instead cannot harm ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Tom Prince's patch to support parametric "constructor n" inGravatar herbelin2011-10-25
| | | | | | tactic notations and ltac definitions (see bug report #2496). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14606 85f007b7-540e-0410-9357-904b9bb8a0f7
* First attempt at making Print Assumption compatible with opaque modules (fix ↵Gravatar letouzey2011-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | #2168) We replace Global.lookup_constant by our own code that looks for a module and enters its implementation. This is still preliminary work, I would prefer to understand more completely the part about module substitutions when entering an applied functor. But this code already appears to work quite well. Anyway, since we only search for constants, we don't need to reconstitute a 100% accurate environment, as long as the same objects are in it. Note: - Digging inside module structures is slower than just using Global.lookup_constant. Hence we try to avoid it as long as we could. Only in front of axioms (or in front of constant unknown to Global) do we check whether we have an inner-module implementation for this constant. There is some memoization of the search for internal structure_body out of a module_path. - In case of inner-module axioms, we might not be able to print its type, but only its long name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
| | | | | | | | | | Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using ↵Gravatar aspiwack2011-09-12
| | | | | | the uid returned by Goal.uid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lib.node: merge OpenedModtype and OpenedModule, same for Closed...Gravatar letouzey2011-09-05
| | | | | | This allows more sharing of code (cf. start_module / end_module) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Porting Hendrik's 8.3 patch for proof tree visualization under proofGravatar herbelin2011-08-30
| | | | | | | | 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
* Quick improvement of some error messages related to module applicationGravatar herbelin2011-08-30
| | | | | | | | (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
* 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
* 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
* 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
* 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
* Term: Refactoring of hashconsingGravatar puech2011-07-29
| | | | | | | - moved the alterate Hashtable module to a separate file - moved all hashconsing-related function to a separate section in Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oversight in revision 14292.Gravatar pboutill2011-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of r14292Gravatar pboutill2011-07-26
| | | | | | No more assertion failure because of half done job. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.Gravatar courtieu2011-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14261 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Check if recursive calls are guarded before printing "Proof completed"."Gravatar pboutill2011-06-10
| | | | | | | | | | | because guard condition is checked at Qed anyway and it can be expensivise to check it twice. Use explicitly "Guarded" if you want this information. But the wrong proof completed is now the right no more subgoals ... Of course, we would like an incrementally checked guard condition one day ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14177 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 17:12:53 +0000