aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-11-18Fix for subclasses implementation, allowing to register generalized classes ↵msozeau
subclasses during type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14678 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
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
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14674 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Merge fix for bug #2604.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14673 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible ↵msozeau
due to dependencies though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14672 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
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
2011-11-17Was missing a potential application of subtypingmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14670 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Adding postprocessing to remove "commutative cuts" expansions inherbelin
pattern-matching when it turns after typing phase that no dependencies exists. Incidentally, renamed regeneralize_index into relocate_index and make it works both way (to generalize and to ungeneralize). This avoids using replace_tomatch for ungeneralization which does not support modifying the "deps". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14669 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Changed the way find_dependencies_signature is working so that itherbelin
applies to terms to match that are not necessarily rel's. Also simplified build_initial_predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14668 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16De Bruijn indices bug in pattern matching compilation in the presenceherbelin
of dependent types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14667 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Old generalization bug in pattern-matching: names were considered theherbelin
same in every branches while they should have been adjusted to the names locally used in the branch. Fixing it by remembering an index of the declaration to abstract in the env together with the declaration itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14666 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
(technically, since the signature "tomatch" of terms to match and of terms to generalize is typed in a context that does not consider terms to match as binders while the return predicate do consider them as binders, the adjusment of the context of the "tomatch" to the context of the predicate needs lifting in each missing part of the "tomatch" context, what was not done) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Old typing bug in pattern-matching compilation (apparently w/oherbelin
consequences up to now, but maybe because this type is often later on thrown away). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14663 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Specialization of tomatch in pattern-matching compilation was done tooherbelin
late for being taken into account in generalized declarations. Do it build_branch as it was for specialization of the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14661 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:19:46 +0000