aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
...
* Fixes mini-bug: Qed would succeed even on focused proofs.Gravatar aspiwack2011-08-12
| | | | | | It allowed proofs of the Shape [{ solve. Qed.] which is inelegant at best. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing typos in commentsGravatar herbelin2011-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Graceful error message for [Proof Mode] and [Set Default Proof Mode] when ↵Gravatar aspiwack2011-08-10
| | | | | | requiring a non-existing proof mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stores bullet stack on locally at the level of focuses rather than globally ↵Gravatar aspiwack2011-07-11
| | | | | | | | in the proof. Fixes bug #2568 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2568 ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14274 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bullets so that they would play well with { }.Gravatar aspiwack2011-07-06
| | | | | | | | | | | | | | | | | | We can now have script like assert P. { destruct n. - solve_case1. - solve_case2. } solve_goal However there is an undesirable interaction with Focus (which we might, anyway, consider deprecated in favour of {}). Indeed, for compatibility with v8.3, Unfocus is called implicitely after each proof command if there is no focused goal. And the new behaviour of bullets is to allow arbitrary unfocusing command "pass trough" them. As a result, a script like Focus. split - solves_first_goal will result in a fully unfocused proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14262 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
| | | | | | | | | particular, new printer for evar_map which displays undefined evars + defined evars that were instantiated by these undefined evars and recursively, up to some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:47:06 +0000