aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
pattern-unification test. They were tolerated up to r14539. Also expanded the let-ins not bound to rel or var in the right-hand side of a term for which pattern-unification is tested (this expansion can refer to a non-let variable that has to be taken into account in the pattern-unification test). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14757 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Fixed a bug introduced in r12755. CoqIDE would ignore the Printing ↵ppedrot
Existential Instances options because it was ill-formed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14756 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Extraction: try to avoid issues with an Include directly inside a .vletouzey
This concerns only "monolithic" extraction (and not Extraction Library). Typical situation is Vector.v containing an Include VectorDef. Cf. the test-case of bug #2570. Also kills two lines of dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14755 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Now CoqIDE relies on the option query mechanism to set printing options. ↵ppedrot
Still a bit hackish. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14754 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30More type safety in query GADT (again).ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14753 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are ↵ppedrot
enforced through hand-made casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14751 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Continuing r14747 being actually incomplete (flushing warnings andherbelin
printing them only if verbose). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14750 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14749 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Preventing Implicit Arguments warning to be shown in non verbose modeherbelin
+ flushing printing of the message . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14747 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Documentation of appcontextletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14744 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Fixed a warning about unused variable introduced in r14731ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14743 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29lib/xml_lexer.ml in .gitignore (produced by a .mll)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14742 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Extraction: typo in last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14741 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29fix for bug #2649corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14740 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Term: properly ignore Casts between Apps in constr_ordpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14739 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Term: useless conversion to list in constr_ord deletedpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14738 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
not in pattern-matching compilation. Also extended to the Var case the preference given to using the term to match as alias rather than its expansion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14737 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28Fixing dependencies postprocessing bug in pattern-matching compilation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14736 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28Term: Fix hash_constr behavior for Cast lnterleaved in application spines.puech
hash_constr should give the same hash to two terms differing only by the presence of Casts. It should now make the same quotients on terms than constr_ord or equals_constr. This handles the case of App(Cast(App(f, l1), _, a), l2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14735 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
The MLcase has notably changed: - No more case_info in it, but only a type annotation - No more "one branch for one constructor", but rather a sequence of patterns. Earlier "full" pattern correspond to pattern Pusual. Patterns Pwild and Prel allow to encode optimized matchs without hacks as earlier. Other pattern situations aren't used (yet) by extraction, but only by P.N Tollitte's code. A MLtuple constructor has been introduced. It isn't used by the extraction for the moment, but only but P.N. Tollitte's code. Many pretty-print functions in ocaml.ml and other have been reorganized git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-28doc: two minor fixes to make my latex happyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14733 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
(bug was introduced in r14703 when postprocessing started to traverse inner cases). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14732 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25Added an API call to retrieve and change the option stateppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14731 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25Separated the toplevel interface into a purely declarative module with ↵ppedrot
associated types (interface.mli), and an applicative part processing the calls (previous ide_intf). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14730 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25Cleaning up XML parsingppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14729 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25avoid relying on weak invariant in cbv.mlbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14728 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Added a function to inspect current option state.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14727 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Fixed the XML parser CDATA handling (and changed the EOL convention of these ↵ppedrot
files which where Windows-like, whoever knows why). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14726 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Fixed some missing options from previous commit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14725 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options ↵ppedrot
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
2011-11-24Moving XML handling to lib directoryppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14723 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Correct direction for definitional typeclassesmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14722 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-23In emacs mode, prints a list of the dependent existential variables introducedaspiwack
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
2011-11-23Adds a pair of function in Evar_util to gather dependent evars in anaspiwack
[evar_map]. We also gather some metadata on these evars: if they are still undefined, and if not, which evars have been used in their (partial) instantiation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14720 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Renamig support added to "Arguments"gareuselesinge
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
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21New Arguments vernaculargareuselesinge
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
2011-11-21Configurable simpl tacticgareuselesinge
The problem that this patch tries to solve is that sometimes the unfolding behaviour of simpl is too aggressive, frequently exposing match constructs. Moreover one may want some constants to never be unfolded by simpl (like in the Math-Comp library where the nosimpl hack is pervasive). Finally, one may want some constants to be volatile, always unfolded by simple when applied to enough arguments, even if they do not hide a fixpoint or a match. A new vernacular command to be indroduced in a following patch attaches to constants an extra-logical piece of information. It declares wich arguments must be checked to evaluate to a constructor before performing the unfolding of the constant (in the same spirit simpl considers as such the recursive argument of an inner fixpoint). Examples: Arguments minus !x !y. (* x and y must evaluate to a constructor for simpl to unfold minus *) (S x - y) --- simpl ---> (S x - y) (S x - S y) --- simpl ---> (x - y) Definition fcomp A B C (f : B -> C) (g : A -> B) x := f (g x). Arguments fcomp A B C f g x /. Infix "\o" := fcomp (at level 50, left associativity) : nat_scope. (* fcomp hides no fix, but simpl will unfold if applied to 6 arguments *) (fun x => (f \o g) x) = f \o g --- simpl ---> (fun x => f (g x)) = f \o g Arguments minus x y : simpl never. (* simpl will never unfold minus *) (S x - S y) --- simpl ---> (S x - S y) Definition nid (x : nat) := x. Arguments nid / x. (* nid is volatile, unfolded by simpl when applied to 0 or more arguments *) nid --- simpl ---> (fun x => x) Arguments minus x y : simpl nomatch. (* triggers for minus the "new" simpl heuristic I discussed with Hugo: if reducing the fix would leave a match in "head" position then don't unfold a suggestion for a better name (for "nomatch") would be appreciated *) (0 - y) --- simpl ---> 0 (S x - y) --- simpl ---> (S x - y) (S x - S y) --- simpl ---> (x - y) (minus 0) --- simpl ---> (minus 0) (* This last test does not work as one may expect, i.e. (minus 0) --- simpl ---> (fun _ => 0) The point is that simpl is implemented as "strong whd_simpl" and after unfolding minus you have (fun m => match 0 => 0 | S n' => ...n' - m'... end) that is already in whd and exposes a match, that of course "strong" would reduce away but at that stage we don't know, and reducing by hand under the lambda is against whd reduction. So further discussion on that idea is needed. *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14716 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21coqide default pref files are by default in /etc/xdg/coq/pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21/home/pirbo/.coqrc* are read againpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14714 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21-user option removalpboutill
it is imcompatible with the freedesktop policy that config directory is private. Feel absolutly free to revert this commit if you think -user should stay git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Updated CHANGES file wrt to pattern-matching compilation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14712 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
to the dependencies in the real arguments (a.k.a. indices) of the terms to match. This allows in particular to make the example from bug report #2404 work. TODO: move the computation of dependencies in compile_branch at the time of splitting a branch (where the computation is done now, it does not allow to support dependent matching on the second argument of a constructor of type "forall b, (if b then Vector.t n else nat) -> Vector.t n -> foo"). TODO: take dependencies in Var's into account and take dependencies within non-Rel arguments also into account (as in "match v (f t) with ... end" where v is a Var and the type of (f t) depends on it). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14711 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Add matching on non-inductive types in building an inversion problemherbelin
for finding the initial predicate, since their type can be dependent on previous terms to match and they may have to be generalized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14710 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Old naming bug in pattern-matching compilation: names in theherbelin
pattern-matching problem generated for the return clause were not the name of patterns (no counter-example though, revealed by using generalization more intensively). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14709 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Inlining let-in (i.e. trace of aliases) in extract_predicate for whatherbelin
seems to provide a better rendering in pattern-matching compilation. Did it also in compile_generalization but not sure the uj_typ is not dropped anyway. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14708 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21VectorDef.v takes benefit of dependencies being taken into accountherbelin
between initial terms to match in pattern-matching compilation algorithm. Also simplified Fin.v though the simplification was possible beforehand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14707 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21In pattern-matching compilation, now taking into account the dependenciesherbelin
between initial arguments (if not rel). Predicate now assumed dependent by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14706 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Simplifying history management in pattern-matching compilation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14704 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:22:12 +0000