aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
...
* fix [Search] when the result has no hypothesis & constant comparisonGravatar puech2010-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
| | | | | | | | | informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve unification when evars and metas are mixed.Gravatar msozeau2010-02-22
| | | | | | | | | If we can't mimick a rhs in an ?evar = rhs situation, we first turn all metas in rhs into evars before trying to solve the equation. Problem reported by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compute the correct generalization information when discharging a classGravatar msozeau2010-02-16
| | | | | | | by a class variable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
| | | | | | | dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
| | | | | | | environment during unification. Should be checked earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing some betaiota-redexes in error messages (an experiment)Gravatar herbelin2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in error messageGravatar herbelin2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix handling of instance declarations in presence of let-ins (bugGravatar msozeau2010-01-01
| | | | | | | reported by Eelis van der Weegen). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2193: computation of dependencies in the "match" returnGravatar herbelin2009-12-30
| | | | | | predicate was incomplete. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12615 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
| | | | | | | | | no longer considered a progress (this prepares generally having tactics with arguments that contains holes that are added to the goal sigma). Incidentally, made that "clear" now restricts evars only if the restriction is really needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
| | | | | | | | Explained in CHANGES how to cope with the change of semantics of abbreviations wrt implicit arguments positions propagation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)Gravatar herbelin2009-12-03
| | | | | | | Removed one more bug in simplification of visibly_occur_id in r12549 + improved CHANGES message git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
| | | | | | | | | | - fixed misunderstanding of the role of nenv while simplifying code of occur_id in namegen.ml, - documented the possible incompatibilites in CHANGES - fixed output/Naming.v test, and fixed the count of misc. tests in test-suite/check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
| | | | | | | | | | | | | | | | | | | | | | - backtrack on incompatibility introduced in intro while trying to simplify the condition about when to restart the subscript of a name (the legacy says: find a new name from x0 if the name xN exists in the context but find a new name from xN+1 if the name xN does not exists in the context but is a global to avoid). - made the names chosen by "intro" compliant with the ones printed in the goal and used for "intros until" (possible source of rare incompatibilities) [replaced the use of visibly_occur_id for printing the goal into a call to next_name_away_in_goal] - also made the names internal to T in "T -> U" printed the same in the goal as they are while printing T after it is introducted in the hypotheses [non contravariant propagation of boolean isgoal in detype_binder] - simplified a bit visibly_occur_id (the Rel and Var cases were useless as soon as the avoid list contained the current env); still this function is costly with polynomial time in the depth of binders - see file output/Naming.v for examples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
| | | | | | | | | | | | Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix type class discharge again.Gravatar msozeau2009-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12526 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on fixing #2167Gravatar herbelin2009-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redoing broken commit r12498 (fixing bug #2167 + attempt to test theGravatar herbelin2009-11-11
| | | | | | | compatibility of a more robust check of unconvertibility when providing "with" arguments to "apply"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2167 + attempt to test the compatibility of a more robustGravatar herbelin2009-11-11
| | | | | | check of unconvertibility when providing "with" arguments to "apply". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12498 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit 12485 continued.Gravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12486 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Took local definitions into account in the test for deciding whetherGravatar herbelin2009-11-08
| | | | | | | | the return clause of match is printed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12480 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix discharge bug in typeclasses: some constrs were not actuallyGravatar msozeau2009-11-06
| | | | | | | | | discharged on the other definitions in the section. - Avoid universe problem in generalize_eqs were we could give an [@eq_refl Set x x] proof where an [@eq Type x x] was expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
| | | | | | | Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted an incorrect code simplification in function status_changedGravatar herbelin2009-11-02
| | | | | | | (rewrote it differently to avoid being trapped again). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to capture on time unification errors for "with" bindings.Gravatar herbelin2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take constraints into account in the "instantiate" tacticGravatar herbelin2009-10-30
| | | | | | | | (building an example that needs it to do). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in dnet.ml, which missed some results when filtering one term ↵Gravatar puech2009-10-29
| | | | | | | | | | against many patterns. Conflicts: lib/dnet.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make usage of Dyn explicitGravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes around typeclasses:Gravatar msozeau2009-10-27
| | | | | | | | | | | | | | - Correct discharge/classify/rebuild for instances. Semantic of Global/Local: local by default in sections, global by default in modules. - Fix the discrimination net's handling of type universes, let the unification do it. - Correct the typeclass resolution tactic so that when extern tactics themselves launch class resolution we don't duplicate work. Problem reported by Arthur Chargueraud. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
* First debug... the renaming of librairies was not working and auto/dn were ↵Gravatar soubiran2009-10-23
| | | | | | not taking in account equivalent names of inductive types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12408 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
| | | | | | | | Compatibility version is now a global parameter that every feature can individually browse. This avoids having to keep the names of options synchronous in their respective files and in now-removed file coqcompat.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
| | | | | | | | | instantiated in tactics (here apply and apply in) that should not open existential goals (see Bas Spitters' coq-club mail about "exists" leaving open existentials). - Preserved the history of the evars occurring in bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
| | | | | | | | | | | | | | 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
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
| | | | | | | | | | | | | | | | | | | rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 15:43:42 +0000