aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2009-09-15Dont't forget to update the state or an obligation tactic assignment maymsozeau
have no effect when the module is later imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12332 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-15Stop using [obligation_tactic] from Program.Tactics as the defaultmsozeau
obligation tactic so that [Program] can work without importing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12330 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
by Context. Now Context has exactly the same semantics as Variables. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-13- Inductive types in the "using" option of auto/eauto/firstorder areherbelin
interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Removed Gappa from the external provers supported by the dp plugin. Tactic ↵gmelquio
gappa has been supported for some time in an external package. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12320 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11- Resolve type class constraints before trying to find unresolvedmsozeau
obligations in [Program Fixpoint]. - Add maximal implicits for pairs in [Program.Syntax]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12319 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-10Misc fixes:msozeau
- better implicits for [antisymmetry] - don't throw away implicit arguments info when doing [Program Definition : type.] - add standard debugging tactics to print goals/hyps in Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12317 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-10Added syntax "exists bindings, ..., bindings" for iterated "exists".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsletouzey
Mostly results about Zgcd (commutativity, associativity, ...). Slight improvement of ZMicromega. Beware: some lemmas of Zdiv/ Znumtheory were asking for too strict or useless hypothesis. Some minor glitches may occur. By the way, some iff lemmas about negb in Bool.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-07ajout CVC3; ajout traduction des reelsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12309 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
setoid_rewrite's code. Cleanup in vernacexpr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12303 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-02Hack to correctly get ill-formed rec body exceptions even msozeau
when the environment is reset. Bug is due to the use of the imperative the_globrevtab when trying to pretty-print the terms involved which may refer to the last defined obligation which is defined in the exception's environment and not the global one anymore. Bug reported by Francois Pottier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12302 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-28update for why 2.19marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12297 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵fbesson
85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-20new csdp cache + improved error messagefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12287 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-20new csdp cache + improved error messagefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14+Fix interface.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12281 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Infix (r12268 continued)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12270 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06Cleaning of Nametab continued + fixed a compilation bug in previous commit.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
(uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-03Added "etransitivity".herbelin
Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Improved parameterization of Coq:herbelin
- add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-31addition of lia.cache - csdp.cache is now handled by micromega not csdpcertfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30micromega : Better parsing of formulae - smaller proof terms for Z - ↵fbesson
redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
I wonder how many of us were aware of the existence of such syntax ;-) Anyway, it is now subsumed by "rewrite by". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12248 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Use camlp4 to accept some specific non-exhaustive patterns in groebnerletouzey
The camlp4 extension "refutpat" provides a syntax let* for pattern that are non-exhaustive on purpose (e.g. let* x::l = foo in ...). A Failure is raised if the pattern doesn't match the expression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Move some examples for groebner into a test-suite fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12244 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
more often but respects the spec better. The changes in the stdlib are reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing conversion with delta on open terms in that case). Also fix a minor bug in typeclasses not seeing typeclass evars when their type was a (defined) evar itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-04repport of commit r12221jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12222 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-29Miscellaneous practical commits: herbelin
- 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
2009-06-29Fix bug introduced by last revision, subtac_cases was returning themsozeau
wrong tycon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12216 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-28Abstract the tycon by the matched terms when turning them into variablesmsozeau
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
2009-06-28Improve return predicate inference by making the return type dependentmsozeau
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
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-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-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-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-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-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-26Fix de Bruijn lifting bug appearing when we match on multiple terms withmsozeau
de Bruijn-bound parameters (reported by W. Swierstra). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12142 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-16Support for definition hooks in subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12126 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-11micromega: proof compression bugfixfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12123 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28More efficient handling of evars in Program Fixpoint commands.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12116 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
clause resulting in stray notations for e.g. variable named "le") and 12083 (fixing bug in as clause of apply in) from trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12103 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24- New cleaning phase for the entry points of pretyping.mlherbelin
- Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml so as to ease the comparison between these files. Application of a change that cannot do harm: j_nf_evar now called after getting evd from consider_remaining_unif_problems in Subtac_pretyping_F.understand_judgment. Four differences remain (is it the sign of a problem?): 1) understand_type fails in Pretyping if evars remain but does not fail in Subtac_pretyping_F 2) resolve_typeclasses (when called) is called with ~onlyargs:false and ~fail:true in Pretyping.understand, Pretyping.understand_gen and Pretyping.understand_type but with true and false in these same functions in Subtac_pretyping_F 3) understand_ltac does not call typeclasses in Pretyping but it does call it in Subtac_pretyping_F 4) understand_judgment does call typeclasses in Pretyping but not in Subtac_pretyping_F git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12099 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16Better Requires in Classes. Fix bug #2093: the code does not requiremsozeau
Program.Tactics anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12089 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16nouvelle version de la tactique groebner proposee par Loic:barras
- algo de Janet (finalement pas utilise) - le hash-cons des certificats de Benjamin et Laurent pas encore integre - traitement des puissances jusqu'a 6 (methode totalement naive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12088 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 17:09:20 +0000