aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Collapse)AuthorAge
* correcting inversion in list of generated tcc of FunctionGravatar letouzey2012-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof using ...Gravatar gareuselesinge2011-12-12
| | | | | | | | | | | | | New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
| | | | | | | | | | | | | | | | | These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove avoidable use of GDynamicGravatar glondu2011-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Equality.injectable which did not detect an equality withoutGravatar herbelin2011-10-22
| | | | | | | | | | | | | | | constructors as non relevant for injection. Also made injection failing in such situation. Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases (observed in the compilation of CoinductiveReals.LNP_Digit). The most probable explanation is that this loop was formerly protected by a failing rewrite which stopped failing after revision 14549 made second-order pattern-matching more powerful. Also suppressed dead code in Invfun.intros_with_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
| | | | | | | | There were some confusion on the role of clear_proofs which was applicable only to the global named_context. Hopefully made things clearer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14517 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
| | | | | | Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction du bug 2047Gravatar jforest2011-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Recdef: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14359 85f007b7-540e-0410-9357-904b9bb8a0f7
* Functional_principles_types: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
| | | | | | | | | | | evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Call process_vernac_interp_error before calling Errors.print inGravatar herbelin2011-06-10
| | | | | | | | plugins so that errors are indeed processed. Not sure this is the best way to do it. Maybe funind should use with_heavy_rollback for delimitating its use of vernac commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14181 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
| | | | | | | Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 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
* 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
* Data structure telling implicits of local variables is a map in theGravatar pboutill2011-02-10
| | | | | | intern_env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 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
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
| | | | | | | | | | | | Rationale: the expansion ignores the TYPED clause when {RAW,GLOB}_TYPED are given. Indeed, in this case, the final type is a consequence of either "INTERPRETED BY" (if given), or the default one based on GLOB_TYPED. This avoids the pitfall of the "raw" argument extension, where the TYPED clause was unused and totally misleading. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
| | | | | | | | perl -pi -e 's/(mk)R(Ref|Var|Evar|PatVar|App|Lambda|Prod|LetIn|Case s|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic|Prop|Type|Fix|CoFix|Struct Rec|WfRec|MeasureRec)/\1G\2/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13758 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 files in funind to respect new conventionsGravatar glondu2010-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 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
* Prepare change of nomenclature rawconstr -> glob_constrGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13742 85f007b7-540e-0410-9357-904b9bb8a0f7
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
| | | | | | | option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0"). Would be simpler if make_apply_entry supported lemmas containing evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Auto-inlining of f_terminate in FunctionGravatar jforest2010-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13496 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
| | | | | | | | | | | | | | Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first component is kept, the second one can be obtained with Tacinterp.eval_tactic. Rationale: these declare parsing rules, and eval_tactic is a semantic action, and therefore should be done in the rule body instead. Moreover, having the glob_tactic_expr and its evaluation captured by these rules was quite confusing IMHO. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
| | | | | | | Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
| | | | | | | | | | These functions are applied much more often without labels than with them (the alternate of adding the label wherever relevant changes 124 lines instead of 41). Moreover, this is more consistent with the Term module and there is no ambiguity in argument types. This commit goes towards elimination of occurrences of OCaml warning 6. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 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
* Report fix bug 2345 from v8.3 (Bad error message when functionalGravatar courtieu2010-09-21
| | | | | | | scheme was called on an unknown function anme). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13445 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
* correcting a bug in funind introduced in r 13292Gravatar jforest2010-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
| | | | | | | to their signature of implicit positions and scopes) is computed. A bit of documentation in constrintern.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration dans FunctionGravatar jforest2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
| | | | | | | thunks. Move from [lazy] to [delayed] in subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
| | | | | | | | | | | | | | a 3 state type to allow: * KernelVerbose / KernelSilent : handle the display of messages launch by Coq * UserVerbose : handle the display of messages launch by user actions Coq will still behaves the same way (TODOs in the code mark the places where we can now change the behaviour). I'll remove them in a few days when we'll have agreed on the correct behaviour. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
| | | | | | | | | | checking function was used instead of a test of existence in the context. Also restricted constr_of_id which had no reason to interpret a posteriori an already interpreted identifier as a global reference. Consequently adapted funind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing to use an ordering different than Lt with measureGravatar jforest2010-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using vernac parsing for FunctionGravatar jforest2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
* better detection of nested recursion in FunctionGravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of a bug pointed by P. Casteran.Gravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Trying to find a problem pointed by P. CasteranGravatar jforest2010-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of bug 2290 (removing stupid message)Gravatar jforest2010-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction of bug 2290Gravatar jforest2010-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12989 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 00:47:33 +0000