aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-05-27dead code pruningvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12143 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-26Fix de Bruijn lifting bug appearing when we match on multiple terms withmsozeau
de Bruijn-bound parameters (reported by W. Swierstra). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12142 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-26ocamldebug-coq: add some forgotten -Iletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12141 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-24Temporary fixes in unification:msozeau
- Solve meta type equations in the order they appeared during unification: it's sensible because we do an [hnf_constr] on these types, introducing a bit of delta even when it's not allowed by the flags, and some code relies on it. A definite solution would involve an nf variant of hnf_constr or allowing delta-reduction of closed terms when unifying types. - Do a bit of betaiota reduction on types in [check_types] while we haven't got a sort-variable aware [is_trans_fconv] test. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12140 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-24Moved and completed the history of Coq versions from theherbelin
revised-theories branch. The V5.10 period at Lyon is still unclear. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12138 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-23A try at using sort variables during unification. Instead of refreshingmsozeau
universes as usual, we add the new universes to the sort constraints and do unification modulo those ([constr_unify_with_sorts]): this allows to instanciate Type i with Prop for example and keep track of it. The sort constraints are thrown away at the end of unification for the moment, but we can detect inconsistencies during unification. Make unification more symmetric as well w.r.t. substitution of defined metas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-20Many fixes in unification:msozeau
- Restore failure when types don't unify in [unify_types] (undoing r12075) but try to be more clever about cumulativity using the meta's [instance_status] information. - Fix second-order abstraction when K is not allowed to ensure that we don't unify twice with the same subterm in [w_unify_to_subterm_list]. A more elaborate solution would be give the list to [w_unify_to_subterm] so that it keeps going when it finds an already-found instantiation. - Two "obvious" errors fixed: taking the wrong instance status when unifying with a meta on the right and forgoting type equations in [w_merge]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12136 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
(bug 2092 and decl_mode.v in test suite). - Added a debugging printer for pftreestate. - Fixing American spelling in RefMan-decl.tex. - Optimizing application of tactic validation by removing consistency test in descend. - Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-19Fix in canonical structure resolution: [check_conv_record] may returnmsozeau
non-matching lists. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12133 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-19Remove camlp4-specific exception handlingmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12132 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-18Minor unification changes:msozeau
- Primitive setup for firing typeclass resolution on-demand: add a flag to control resolution of remaining evars (e.g. typeclasses) during unification. - Prevent canonical projection resolution when no delta is allowed during unification (fixes incompatibility found in ssreflect). - Correctly check types when the head is an evar _or_ a meta in w_unify. Move [isEvar_or_Meta] to kernel/term.ml, it's used in two places now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12131 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-17- Allowing multiple calls to tactic fix with automatic generation ofherbelin
function name (instead of failure). - Making descent through conjunctions in apply work on recursive tuples such as Acc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12129 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-16(Tentative to) add Canonical Structure resolution to the regularmsozeau
unification algorithm. Uses the same code to recognize projections (check_conv_record) and the same unification steps on the solution as evar_conv. This required to fold the sigma through unify_* along with the meta and evar substitutions as this can grow during unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12128 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-16Minor fixes in typeclasses:msozeau
- Set implicit args on for Context decls - Move class_apply tactic to Init - Normalize evars before raising an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-16Support for definition hooks in subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12126 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-13 Fix to my last notation patch: now fixpoint are correctly handled vsiles
when it comes to notation declared in scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12125 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-13minor bugfixes. CoqIde development will resume soon now ...vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12124 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-11micromega: proof compression bugfixfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12123 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
revealed a too strict test for detection of inferable metas in Clenv. Restored tolerance for unbound names in interactive tactic use. - Moral removals of some captures of Not_found in Environ.evaluable_* since kernel is assumed to deal with existing names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-09fix a bug in canonical structures (bug found and fixed by Cyril)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12120 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-07adds a theorem to reason at the level of Zbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12119 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-05Improvements in typeclasses eauto and generalized rewriting:msozeau
- Decorate proof search with depth/subgoal number information - Add a tactic [autoapply foo using hints] to call the resolution tactic with the [transparent_state] associated with a hint db, giving better control over unfolding. - Fix a bug in the Lambda case in the new rewrite - More work on the [Proper] and [subrelation] hints to cut the search space while retaining completeness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12118 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-30Fix a small notation/scope bug:vsiles
When defining an inductive type with a reserved notation in a particuliar scope, the scope was not opened during the interpretation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12117 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28More efficient handling of evars in Program Fixpoint commands.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12116 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28Fixes for bugs in r12110:msozeau
- [matches] is not parameterized by evars: normalize before calling conclPattern. - fix hints in Morphisms for subrelation and handling of signature normalization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12115 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28_tags: lexer.ml4 now uses pa_macroletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12114 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28Backporting 12112 from v8.2 branch to trunk (fixing documentation bugsherbelin
#2099 in ConstructiveEpsilon.v and #2100 on Global Opaque). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12113 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27Cleanup old eauto code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12111 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Implementation of a new typeclasses eauto procedure based on successmsozeau
and failure continuations, allowing to do safe cuts correctly. - Fix bug #2097 by suppressing useless nf_evars calls. - Improve the proof search strategy used by rewrite for subrelations and fix some hints. Up to 20% speed improvement in setoid-intensive files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12110 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
- Added support for list of intropattern in Tactic Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12109 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
- Adding test file related to commit 12080 (bug #2091). - Cleaning old parsing stuff from 8.0. - Support for camlp5 in base_include. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Report de la révision #12104 (Maj lien site web de Coq)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12105 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
clause resulting in stray notations for e.g. variable named "le") and 12083 (fixing bug in as clause of apply in) from trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12103 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
the interpretation mechanism of ltac variables) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12100 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24- New cleaning phase for the entry points of pretyping.mlherbelin
- Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml so as to ease the comparison between these files. Application of a change that cannot do harm: j_nf_evar now called after getting evd from consider_remaining_unif_problems in Subtac_pretyping_F.understand_judgment. Four differences remain (is it the sign of a problem?): 1) understand_type fails in Pretyping if evars remain but does not fail in Subtac_pretyping_F 2) resolve_typeclasses (when called) is called with ~onlyargs:false and ~fail:true in Pretyping.understand, Pretyping.understand_gen and Pretyping.understand_type but with true and false in these same functions in Subtac_pretyping_F 3) understand_ltac does not call typeclasses in Pretyping but it does call it in Subtac_pretyping_F 4) understand_judgment does call typeclasses in Pretyping but not in Subtac_pretyping_F git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12099 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-21fixed CBV strategy: it was too eager on terms likebarras
Axiom f: (nat->nat)->Prop. Eval compute in let _ := f(fun _ => mult 1000 1000) in 0. function was strongly evaluated when applied to f (based on examples provided by Damien Pous) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12098 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-21Rename [Morphism] into [Proper] and [respect] into [proper] to complymsozeau
with standard math nomenclature. Also clean up in rewrite.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12097 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-20Fix test output mentionning an existential number that changed.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12096 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-20Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatmsozeau
Setoid doesn't export Program.Basics anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12095 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-18Just export RelationClasses for [Equivalence] through Setoid.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12094 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-17Only export the notations of Morphism as well as Equivalence throughmsozeau
Setoid, the rest needs to be qualified. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12093 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-17- Fix handling of clauses in setoid_rewrite to rewrite under bindersmsozeau
correctly. - Fix the new autorewrite to implement the (unstated) invariant that the last declared rules are applied first, which makes a difference for non-confluent rewrite rules. Some scripts in CoLoR rely on that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12092 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16comparison functions on lists and arraysbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12091 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16Fix bug #2089: correctly dealing with parameters and real arguments inmsozeau
Combined Scheme. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12090 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16Better Requires in Classes. Fix bug #2093: the code does not requiremsozeau
Program.Tactics anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12089 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16nouvelle version de la tactique groebner proposee par Loic:barras
- algo de Janet (finalement pas utilise) - le hash-cons des certificats de Benjamin et Laurent pas encore integre - traitement des puissances jusqu'a 6 (methode totalement naive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12088 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-14Rewrite autorewrite to use a dnet indexed by the left-hand sides (ormsozeau
rhs) of rewrite lemmas for efficient retrieval of matching lemmas. Autorewrite's implementation is still unchanged but the dnet can be used through the [hints] strategy of the new generalized rewrite. Now lemmas are checked to actually be rewriting lemmas at declaration time hence the change in DoubleSqrt where some unapplicable constants were declared as lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12087 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-14Add a combinator for rewriting given a list of terms and fix themsozeau
top-down strategy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12086 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 18:31:00 +0000