aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-06-26Add doc for [Print Opaque Dependencies] and a better explanation for themsozeau
flags of manual implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22Correct treatment of dependent products in signatures: create the evarsmsozeau
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
2009-06-22Fixes for r12197, the refined evars were not returned in case fail_evarmsozeau
was true. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22documented a bug of pattern unification with metasbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12203 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22made several occurrences of (eapply ...; eauto) not rely on the lack of ↵barras
pattern unification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12202 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22Report de la révision #12200 (bug #2125)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12201 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22remove some unused functions (which are part of a soon-to-be obsoletevgross
framework anyway) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12199 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22clearing unused functionsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12198 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-18Use more consistent resolution parameters in Program and regular typingmsozeau
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
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
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
2009-06-18Try typeclass resolution in coercion if no solution can be found to amsozeau
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
2009-06-17Fallback on not using [fix_proto] if the right imports aren't there, the msozeau
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
2009-06-16Reimplementation of leibniz rewrite to control the instantiation of themsozeau
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
2009-06-15Allow anonymous instances again, with syntax [Instance: T] where Tmsozeau
may be a product. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12188 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-13Correct typo: -noglob takes no argument.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12186 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
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
2009-06-11Simplifying the call to print_no_goals and not calling it when no goalherbelin
is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-11When typing a non-dependent arrow, do not put the (anonymous) variablemsozeau
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
2009-06-10Accept more Unicode symbolsglondu
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
2009-06-10Use the projections for reflexivity, symmetry and transitivity proofs tomsozeau
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
2009-06-09Correct handling of the initial existentials from the goal and the onesmsozeau
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
2009-06-08Do a fixpoint on the result of typeclass search to force themsozeau
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
2009-06-08Change in UI behaviour : proof folding is now done by double clicking. Delay isvgross
configurable through preferences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12174 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-07File forgotten in commit 12171.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12173 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-07Partial simplification of undo mechanism, relying only on Courtieu'sherbelin
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
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
- "*" 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
2009-06-06Makefile made compatible with Solaris 10 (bug #2078, continued - seeherbelin
revisions 12063 and 12065). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12169 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
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
2009-06-06Fixing bug #2106 ("match" compilation with multi-dependent constructor).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12167 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-06Very-small-step policy changes to the library.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12166 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-06Applying Ian Lynagh's documentation fixes patch (see bug #2112)herbelin
[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
2009-06-03Ensure the precondition of the partial function [list_chop] holdsmsozeau
before calling it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12162 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-02Adding a regression test about Bauer's example on coq-club ofherbelin
rewriting using eta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12161 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-02Use Type instead of Set.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12160 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-02Backtrack on experimental unification with sort variables: it requires msozeau
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
2009-06-02Fix script file using the "Manual Implicit" flag.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12158 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-01## Lines starting with '## ' will be removed from the log message.msozeau
## File(s) to commit: ## tactics/refine.ml Try solving typeclasses before refining in Refine.refine (suggested by S. Lescuyer). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12157 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-01Change unification with sort constraints to not use the kernelmsozeau
conversion when sort variables are involved and always call it with an empty sort constraint set to avoid [whd_sort_variable] reducing a universe variable to an algebraic universe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12156 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-01Prevent automatic inference of implicit arguments when the auto flag ismsozeau
not set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12155 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-29Fix extract hyps to correctly discharge all hyps as described by keepmsozeau
lists. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12154 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-28Properly catch sort constraint inconsistency exception inmsozeau
[base_sort_conv] and revert change in [unify_type]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12153 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-28Adapted the emacs mode to font-lock. Re-using code from ProofGeneral.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12152 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-28Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionaspiwack
qui permet de changer la façon dont on imprime certains sous-termes sans avoir à réécrire entièrement un printer de constr. Dans le même esprit que les commits sur le parser et le lexer, je cherche à donner une flexibilité aux plugins pour changer l'aspect de Coq pour le plier à d'autres conventions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12151 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
definitions and variables (may increase the vo's size a bit), which in turn fixes discharging with manual implicit args only. Fix Context to correctly handle "kept" assumptions for typeclasses, discharging a class variable when any variable bound in it is used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12150 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Populate the sort constraints set correctly during unification. Add amsozeau
[set_eq_sort_variable] for cases where two universes should be equal, fix [evars_reset_evd] to keep sort constraints and use [whd_sort_var] directly in [whd_evar]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12149 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
as they are used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12148 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansaspiwack
un plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12147 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Ma ↵aspiwack
lheureusement,=20je=20ne =20sais=20pas=20permettre=20que=20GDELETE=5FRULE=20soit=20appelable=20pendant=20une=20section =20sans=20causer=20de=20potentiels=20soucis=20(bien=20que=20je=20trouve=20qu'il=20faille=20un =20esprit=20sacr=C3=A9ment=20pervers=20pour=20faire=20Declare=20ML=20Module=20dans=20une=20section).?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Je suppose qu'on est dans le même esprit d'information trop partielle que pour les notations aux niveaux 8, 99 et 200. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12146 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27sane behaviour for copy/paste operations (the code is still insane, though)vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12145 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27keeping interface synch'edvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12144 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:22:08 +0000