aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Fixed anomaly when trying to load non existing file starting with "./" or "../".Gravatar herbelin2009-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2129 (evar introduced to remember an ambiguous projectionGravatar herbelin2009-07-08
| | | | | | | | | had wrong type). At least two problems remain: - projection involving evar should check the type are compatible, - instances of filtered evars should not be shrinked as all values are needed to ensure the well-typedness of the instanciated restricted evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completing support for F5=About by adding About to the state-preserving ↵Gravatar herbelin2009-07-08
| | | | | | command list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
| | | | | | | | | traînaient un peu partout dans le code depuis la fusion d'evar_map et evar_defs. Début du travail d'uniformisation des noms donnés aux evar_defs à travers le code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
* change in the order of unification constraints solving (for canonical ↵Gravatar amahboub2009-07-06
| | | | | | structures) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12223 85f007b7-540e-0410-9357-904b9bb8a0f7
* repport of commit r12221Gravatar jforest2009-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
| | | | | | | | | | | | | | | selection of occurrences. We use a new function [unify_to_subterm_all] to return all occurrences of a lemma and produce the rewrite depending on a new [conditions] option that controls if we must rewrite one or all occurrences and if the side conditions should be solved or not for a single rewrite to be successful. [rewrite*] will rewrite the first occurrence whose side-conditions are solved while [autorewrite*] will rewrite all occurrences whose side-conditions are solved. Not supported by [setoid_rewrite] yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
| | | | | | | | | | | | - theories: made a hint database with the constructor of eq_true - coqide: binding F5 to About dans coqide + made coqide aware of string interpretation inside comments - lexer: added warning when ending comments inside a strings itself in a comment - xlate: completed patten-matching on IntroForthComing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug introduced by last revision, subtac_cases was returning theGravatar msozeau2009-06-29
| | | | | | | wrong tycon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12216 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raise an error and not an anomaly if a rewrite is attempted on aGravatar msozeau2009-06-28
| | | | | | | dependent argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12215 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstract the tycon by the matched terms when turning them into variablesGravatar msozeau2009-06-28
| | | | | | | in Program's pattern-matching compilation (fixes bug #2131). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12214 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve return predicate inference by making the return type dependentGravatar msozeau2009-06-28
| | | | | | | | on a matched variable when it is of dependent type, when its type allows it (no constructor in the real arguments). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12213 85f007b7-540e-0410-9357-904b9bb8a0f7
* propagation sur le trunk du commit 12101 Gravatar soubiran2009-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12212 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
| | | | | | | flags of manual implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct treatment of dependent products in signatures: create the evarsGravatar msozeau2009-06-22
| | | | | | | | | in the right environment and substitute the actual argument in the remaining signature. It works as long as we do no try to rewrite a dependent argument itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
| | | | | | | was true. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
* documented a bug of pattern unification with metasGravatar barras2009-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12203 85f007b7-540e-0410-9357-904b9bb8a0f7
* made several occurrences of (eapply ...; eauto) not rely on the lack of ↵Gravatar barras2009-06-22
| | | | | | pattern unification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12202 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #12200 (bug #2125)Gravatar notin2009-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12201 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove some unused functions (which are part of a soon-to-be obsoleteGravatar vgross2009-06-22
| | | | | | framework anyway) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12199 85f007b7-540e-0410-9357-904b9bb8a0f7
* clearing unused functionsGravatar vgross2009-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
| | | | | | | | and add an optional fail_evar flag to control resolution better in interpretation functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12197 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
| | | | | | | | necessary information. Fix implementation of [split_evars] and use splitting more wisely as it has a big performance impact. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12196 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try typeclass resolution in coercion if no solution can be found to aGravatar msozeau2009-06-18
| | | | | | | | conversion problem. TODO: The right fix is to use constraints and backtracking search when solving them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fallback on not using [fix_proto] if the right imports aren't there, the Gravatar msozeau2009-06-17
| | | | | | | tactics that use it won't be in scope either. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12193 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
| | | | | | | | | | rewriting lemma more precisely. This should make rewrite properly fail when existentials are around instead of giving an identical goal up to new evars. Also a first step towards adding occurences to the leibniz rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
| | | | | | | may be a product. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct typo: -noglob takes no argument.Gravatar msozeau2009-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
| | | | | | | | | | unnecessarily computed when the user won't see it (avoids the costly nf_evar_defs in typeclass errors). Add hook support for mutual definitions in Program. Try to solve only the argument typeclasses when calling [refine]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
| | | | | | | | is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
* When typing a non-dependent arrow, do not put the (anonymous) variableGravatar msozeau2009-06-11
| | | | | | | | | | | in the context to avoid it being abstracted over in potential evars occuring in the codomain, which can prevent unifications. Add [intro] to the typeclasses eauto and fix [make_resolve_hyp] to properly normalize types w.r.t. evars before searching for a class in an hypothesis. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12182 85f007b7-540e-0410-9357-904b9bb8a0f7
* Accept more Unicode symbolsGravatar glondu2009-06-10
| | | | | | The comment just below makes me think this is just a typo... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use the projections for reflexivity, symmetry and transitivity proofs toGravatar msozeau2009-06-10
| | | | | | | | | ensure the type and relation used in the subgoals stay syntactically the same, for compatibility with [ring] which does not use conversion to find the ring on a relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12179 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of the initial existentials from the goal and the onesGravatar msozeau2009-06-09
| | | | | | | coming from the lemma in setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
| | | | | | | resolution of generated evars, not doing any backtracking yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change in UI behaviour : proof folding is now done by double clicking. Delay isGravatar vgross2009-06-08
| | | | | | | | configurable through preferences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12174 85f007b7-540e-0410-9357-904b9bb8a0f7
* File forgotten in commit 12171.Gravatar herbelin2009-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial simplification of undo mechanism, relying only on Courtieu'sGravatar herbelin2009-06-07
| | | | | | | marks and no longer on old-fashioned reset to id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12172 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
| | | | | | | | | | | | | | - "*" implements Arthur Charguéraud's "introv" - "**" works as "; intros" (see also "*" in ssreflect). - Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui. - Shy attempt to seize the opportunity to clean Zarith_dec but Coq's library is really going anarchically (see a summary of the various formulations of total order, dichotomy of order and decidability of equality and in stdlib-project.tex in branch V8revised-theories). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile made compatible with Solaris 10 (bug #2078, continued - seeGravatar herbelin2009-06-06
| | | | | | revisions 12063 and 12065). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
| | | | | | | instead of the index required by the user; extended FixRule and Cofix accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Very-small-step policy changes to the library.Gravatar herbelin2009-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Ian Lynagh's documentation fixes patch (see bug #2112)Gravatar herbelin2009-06-06
| | | | | | | | [copy of revision 12164 from branch v8.2] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensure the precondition of the partial function [list_chop] holdsGravatar msozeau2009-06-03
| | | | | | | before calling it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
| | | | | | | rewriting using eta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use Type instead of Set.Gravatar msozeau2009-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12160 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on experimental unification with sort variables: it requires Gravatar msozeau2009-06-02
| | | | | | | | major changes in [w_unify] and the conversion functions used by it to handle the sort constraints correctly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12158 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 11:48:53 +0000