aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* 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
* Fix bug #2227Gravatar msozeau2011-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix inductive coercion code in Program (bug #2378)Gravatar msozeau2011-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
| | | | | | for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 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
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 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
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
| | | | | | | function but also restricting it to closed matching and consequently renaming it to subst_closed_term_occ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14498 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix commit 14489: missing Coq. in dirpathGravatar letouzey2011-09-23
| | | | | | Kudos to Tom Prince for noticing this... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Program: add some check_required_library (fix #2592) + some dead code removalGravatar letouzey2011-09-23
| | | | | | | | | | | | | If these additional checks take too much time, maybe using true laziness instead of (fun () -> ...) could help. Btw, some other init_constant in Program would deserve preliminary check_required_library... I've also removed some unused delayed constr, at least one of them being erroneous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
| | | | | | | | | | | | | | | | | | This way, no more error messages like "Unrecognized predicate". Some code simplification and reorganization on the way, in particular a few tests like "is_Prop ..." or "closed0 ..." were actually useless. Also add support for the situation H:~Zne x y for uniformity. Beware: scripts relying negatively on the strength of omega may have to be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails."). For instance, one line deletion in PermutSetoid.v Probably more cumbersome : "auto with *" becomes stronger since it may call omega. Todo : check the impact on contribs tomorrow. Btw, this commit seems to solve a bug where omega was to be guided by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Omega aware of Z.pred (fix #1912)Gravatar letouzey2011-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 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
* Improved ltac code for zify (fix #2575).Gravatar letouzey2011-09-06
| | | | | | | | Note nonetheless that the underlying bug is still active (cf. #2602), I've just written the ltac stuff in a nicer way (no nested match goal), and things happen to work now :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14461 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Implicit: fix the numbering of constructor argumentsGravatar letouzey2011-09-05
| | | | | | | | | | | | | | | | | | | | For constructors, the numbers of parameters used to be wrongly ignored. Consider for instance : Inductive listn (A:Type) : nat -> Type := | niln : listn A 0 | consn : forall n, A -> listn A n -> listn A (S n). Saying "Extraction Implicit consn [n]" should now work correctly, and correspond to the alternative syntax "Extraction Implicit consn [2]", where 2 is the position of the argument n when counting with inductive parameters. Note that saying "Extraction Implicit consn [1]" (or [A]) is now a no-op : constructors have always been cleaned-up from their parameters during extraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2589: Documentation patch of Hendrik TewsGravatar pboutill2011-09-02
| | | | | | + s/cbv/lazy of bug 2542 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: allow extraction of records with anonymous fields (fix #2555)Gravatar letouzey2011-08-25
| | | | | | | | | | For Ocaml, we now use the extraction-reserved substring "__" : The name foo__i will be pick for i-th field of record foo if it is anonymous. For Haskell, still no printing of records as native records, hence nothing to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
| | | | | | a smaller risk that "rewrite" clashes with a name used for constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
| | | | | | | Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
* moins de reification inutile, noatations standardsGravatar pottier2011-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring: replaced various generic = on constr by eq_constr, destructors etc.Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quote: replaced various generic = on constr by eq_constr, destructors etc.Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Newring: generic = on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_micromega: generic = on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Field: generic Gmap on constr replaced by CmapGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract_env: generic = on prec_declaration replaced by prec_declaration_equalGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: replace generic = on mutual_inductive_body by mib_equalGravatar puech2011-07-29
| | | | | | Term: add function eq_rel_declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14366 85f007b7-540e-0410-9357-904b9bb8a0f7
* replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac_cases: replaced some generic = on constr by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring: replaced some generic Pervasives.compare on constr by constr_ordGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nsatz: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14360 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
* FourierR: replaced some generic Hashtbl on constr by ConstrhashGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refl_omega: replaced generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Newring: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refl_omega: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Const_omega: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14354 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
* Newring: replaced generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_omega: replaced generic = on constr by eq_constrGravatar puech2011-07-29
| | | | | | Util: Added list_assoc_f git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14350 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quote: replaced generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_omega: replaced many generic = on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Newring: generic Pervasives.compare on constr replaced by constr_ordGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: moved function constr_ord (a.k.a compare_constr) from Sequent to TermGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by ↵Gravatar puech2011-07-29
| | | | | | | | Constrhash and Termhash We need a function hash_constr (added in Term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Newring: generic equality on constr replaced by constr_equalGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14343 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 06:39:09 +0000