aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14703 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Removing stuff about alias dependencies now become useless.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14702 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
main criterion is to look at whether the alias to the term to match is dependent in the return predicate or not. Since the exact return predicate is often found late, the detection is done after the subproblem is fully compiled, when a maximum amount of (local) information on typing is known. Eventually, we should go to a model where all possible partial expansions of an alias are usable at typing time. Indeed the current heuristic (like the previous one) is not fully safe since it might decide not to expand an alias in a branch whose type does not depend of the alias but the typing of the branch internally needs the expansion (as e.g. in "fun (H:forall n, n=0->Prop) n => match n with 0 as x => H x eq_refl | _ => True end"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14701 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Updating Cases.v test.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14700 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Dead code + refreshing some comments in cases.ml.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14699 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14698 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20CHANGES updatepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14697 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coqide-gtk2rc not dottedpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14695 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20CoqIdE configuration file won't pollute your home anymorepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20Teach coq_makefile how to install into XDG_DATA_HOME.pboutill
From Tom Prince. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14693 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coq_makefile: Don't install with +x.pboutill
By Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14691 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coq_makefile: Add Makefile variables specifying installpboutill
paths. By Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14690 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14689 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Fix parsing of :>> and backtrack correctly on the cache of hints for local ↵msozeau
contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14688 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Return of the tactic hints features in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14687 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Added hint support in the API. You can now query a goal to see the tactics ↵ppedrot
that may be used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14686 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Toplevel loop is a bit more robust: it catches bad API queries.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14685 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Making status info better in CoqIDE: path and name of current lemmappedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14684 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. ↵ppedrot
Answers are semantic and not simple strings anymore. Still to be ameliorated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14683 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Added a printing function to handle single evarsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14682 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in ↵ppedrot
CoqIDE (* FIXME *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14681 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Coqide -debug only printed Coqtop information.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14680 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class ↵msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:41:28 +0000