aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
...
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
| | | | | | | | | | use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
| | | | | | | | | strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
| | | | | | | | - seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Catch AbstractionOverMeta as a unification failure in precatchable_exception.Gravatar msozeau2011-06-07
| | | | | | Allows rewrite H in * |- to work in case a rewrite throws this exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Break circular dependency Proof_global -> Vernacexpr -> Proof_global.Gravatar aspiwack2011-05-17
| | | | | | Fixes bug #2547 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2547 ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug in [maximal_unfocus] introduced in r14120.Gravatar aspiwack2011-05-17
| | | | | | Fixes bug #2546 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2546­ ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14130 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better procedure for checking presence of undefined evars.Gravatar aspiwack2011-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
* The modules in proofs now use the Errors module to explain their exceptions ↵Gravatar aspiwack2011-05-13
| | | | | | to the toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14120 85f007b7-540e-0410-9357-904b9bb8a0f7
* New option [Set Bullet Behavior] allows to select the behaviour of bullets.Gravatar aspiwack2011-05-13
| | | | | | | | | - Two predefined behaviours : "None" where bullet have no effect and "Strict Subproofs" (default) which acts as previously. - More behaviours can be registered by plugins via [Proof_global.Bullet.register_behavior]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14118 85f007b7-540e-0410-9357-904b9bb8a0f7
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
| | | | | | | | | | "apply" unification. Assuming w_unify_0 is not eventually abandoned, it remains to merge unify_with_eta into unify_0 (what unify_with_eta does and that unify_0 does not do is to select of two instances of the same meta the one with less lambda's; it is unclear whether this is useful heuristic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug causing inconsistent states during proof editting.Gravatar aspiwack2011-04-29
| | | | | | | | | Some toplevel commands (for instance the experimental bullets) are composed of several atomic commands, the failure of one must imply the failure of the whole toplevel command. This commit introduces a system of transaction to that effect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some comments.Gravatar aspiwack2011-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14086 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
| | | | | | | | | | | This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Tom Prince's patch for build_constant_by_tactic not able toGravatar herbelin2011-04-08
| | | | | | use a lemma name chosen by the caller (here tclABSTRACT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
| | | | | | | | | | | | | | Note: even if this new tactical can be quite handy during the development phase, (for instance to bound the time allocated to some search tactics), please be aware of its main drawback: with it, scripts are no longer machine-independant, something that works on a quick machine may fail on a slow one. The converse is even possible if you combine this "timeout" with other tactic combinators. We strongly advise to not leave any "timeout" in the final version of a development. In addition, this feature won't probably work on native win32, since Unix.alarm isn't implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
| | | | | | | | | | | | | | | | conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
| | | | | | | in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
| | | | | | | unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
| | | | | | | | error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to fix the behavior of clenv_missing used when declaring hintsGravatar letouzey2011-02-22
| | | | | | | | | | | | | Before this patch, hints such as "Hint Resolve -> a" in success/Hints.v were erroneously considered "eauto-only". We try to clarify the big boolean expression via "if", and for the moment we remove the detection of "nonlinearity" via duplicated_metas : on the example, some nonlinearity was found for strange reason (beta expansion ?), and after some discussion with Hugo, it is unclear whether this nonlinearity stuff is useful at all. The next coqbench might provide some answer to this question, we'll see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13850 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Started to fix the declarative proof mode (C-zar).Gravatar aspiwack2011-02-10
| | | | | | | Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported). However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
| | | | | | | | | | | new proof engine. Correct treatment of the evar set: the tactic incrementally extends (and potentially refines) the existing sigma and the internally generated typeclasses constraints are removed from it at the end as they are always solved. This avoids tricky and costly evar_map manipulations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
| | | | | | | | | perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clenv.connect_clenv without its Evd.foldGravatar letouzey2010-12-15
| | | | | | | | | | | Apparently, it seems that clenv.evd is either created from dummy_goal (in (e)auto) or from a copy of gls (in class_tactics). I've checked experimentally by some assert that on the stdlib the defined part of clenv.evd is always included in gls. I hence propose to simplify this function connect_clenv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefinedGravatar letouzey2010-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to preserve casts during a refine, especially VMcastGravatar letouzey2010-12-10
| | | | | | placed by vm_cast_no_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
| | | | | | | before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix minor typo in error message (Closes: #2408)Gravatar glondu2010-10-25
| | | | | | Patch from Adam Megacz. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove open_subgoals field of proof_treeGravatar glondu2010-10-06
| | | | | | It looks obsolete, probably as a consequence of the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13504 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
| | | | | | | governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
| | | | | | | | | | | | | | user either gives all missing arguments not dependent in the concl or all missing arguments not *recursively* dependent in the concl (as introduced by commit 13367). In practice, this means that "apply f_equal with A" remains allowed even though the new, recursive, analysis detects that all arguments of f_equal are inferable, including the first type argument (which is inferable from the knowledge of the function). Sized the opportunity to better explain the behavior of clenv_dependent. Also made minor code simplification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
| | | | | | | | | | dependent arguments. It breaks compatibility as some [apply with] clauses are not necessary anymore. Typically when applying [f_equal], the domain type of the function can be infered even if it does not appear directly in the conclusion of the goal. Fixes bug #2154. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
| | | | | | engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13300 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
| | | | | | enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
| | | | | | | | | | generalize the interface of Clenv to be able to use the existing treatment of bindings. Clenv functions did not use goals conclusions but insisted on getting goals anyway (which is even more problematic as goals appear in evar maps now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
| | | | | | | | | | Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix commentGravatar glondu2010-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 09:03:52 +0000