aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2008-03-28Improve error handling and messages for typeclasses. msozeau
Add definitions of relational algebra in Classes/RelationClasses including equivalence, inclusion, conjunction and disjunction. Add PartialOrder class and show that we have a partial order on relations. Change SubRelation to subrelation for consistency with the standard library. The caracterization of PartialOrder is a bit original: we require an equivalence and a preorder so that the equivalence relation is equivalent to the conjunction of the order relation and its inverse. We can derive antisymmetry and appropriate morphism instances from this. Also add a fully general heterogeneous definition of respectful from which we can build the non-dependent respectful combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
[in I] := t [return pred] in b", just as SSReflect does with let:. Change implementation: no longer a separate AST node, just add a case_style annotation on Cases to indicate it (if ML was dependently typed we could ensure that LetPatternStyle Cases have only one term to be matched and one branch, alas...). This factors out most code and we lose no functionality (win ! win !). Add LetPat.v test suite. - Slight improvement of inference of return clauses for dependent pattern matching. If matching a variable of non-dependent type under a tycon that mentions it while giving no return clause, the dependency will be automatically infered. Examples at the end of DepPat. Should get rid of most explicit returns under tycons. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-27Various fixes on typeclasses:msozeau
- Better interface in constrintern w.r.t. evars used during typechecking - Add "unsatisfiable_constraints" exception which gives back the raw evar_map that was not satisfied during typeclass search (presentation could be improved). - Correctly infer the minimal sort for typeclasses declared as definitions (everything was in type before). - Really handle priorities in typeclass eauto: goals produced with higher priority (lowest number) instances are tried before other of lower priority goals, regardless of the number of subgoals. - Change inverse to a notation for flip, now that universe polymorphic definitions are handled correctly. - Add EquivalenceDec class similar to SetoidDec, declaring decision procedures for equivalences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-21Correct bug introduced in r10589, where we lost information thatmsozeau
assumption types are types when type-checking them and necessary coercions were not inserted. Add empty_evar_defs definition in Evd and call the new helper function in constrintern that performs interpretation and gives back implicit argument information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10706 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
names, gives the ability to specify qualified classes in instance declarations. Use that in the class_tactics code. Refine the implementation of classes. For singleton classes the implementation of the class becomes a regular definition (into Type or Prop). The single method becomes a 'trivial' projection that allows to launch typeclass resolution. Each instance is just a definition as usual. Examples in theories/Classes/RelationClasses. This permits to define [Class reflexive A (R : relation A) := refl : forall x, R x x.]. The definition of [reflexive] that is generated is the same as the original one. We just need a way to declare arbitrary lemmas as instances of a particular class to retrofit existing reflexivity lemmas as typeclass instances of the [reflexive] class. Also debug rewriting under binders in setoid_rewrite to allow rewriting with lemmas which capture the bound variables when applied (works only with setoid_rewrite, as rewrite first matches the lemma with the entire, closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal [exists x, P (f x)]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-17Add the possibility of specifying constants to unfold for typeclassmsozeau
resolution. Add [relation] and Setoid's [equiv] as such objects. Considerably simplify resolve_all_evars for typeclass resolution, adding a further refinement (and hack): evars get classified as non-resolvable (using the evar_extra dynamic field) if they are turned into a goal. This makes it possible to perform nested typeclass resolution without looping. We take advantage of that in Classes/Morphisms where [subrelation_tac] is added to the [Morphism] search procedure and calls the apply tactic which itself triggers typeclass resolution. Having [subrelation_tac] as a tactic instead of an instance, we can actually force that it is applied only once in each search branch and avoid looping. We could get rid of the hack when we have real goals-as-evars functionality (hint hint). Also fix some test-suite scripts which were still calling [refl] instead of [reflexivity]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10687 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-17* Factorizing code : context_chop was used in several files (even as ↵vsiles
chop_context) so I moved it to termops.ml * Fixing a little bug in the Boolean to Leibniz transition in automatic boolean declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10686 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-16Using the "relation" constant made some unifications fail in the newmsozeau
setoid rewrite. Refine and use the new unification flags setup by Hugo to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean indicating conversion is wanted to a Cpred representing the constants one wants to get unfolded to have more precise control. Add corresponding test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10684 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-15Application de refresh_universes dans typing.ml et retyping.ml : lesherbelin
appels à type_of et get_type_of sont souvent utilisés pour construire des termes à partir de types; on ne rajoute pas non plus de contraintes inutiles parce que type_of et get_type_of ne changent pas le graphe de contraintes; tout ce qu'on perd est une information utilisateur sur le type en lui-même mais puisque pretty.ml n'appelle ni type_of ni get_type_of, ces informations sur la représentation interne des univers restent a priori accessibles pour l'utilisateur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-11Typo commit 10653herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10654 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-10Pas très propre de reposer sur la capture des anomalies (et celaherbelin
complique le débogage...). Réécriture de 2 morceaux de code qui utilisaient les anomalies à des fins détournées de leur intention. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10653 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-10fold travaille maintenant sur la forme beta-iota-zeta réduite duherbelin
corps de la constante (comme unfold le fait ici), de telle sorte que "unfold f; fold f" marche (cf bug 1789) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10652 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
- Correction bug des filtres dans define_evar_as_abstraction - Nettoyage, documentation et réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10650 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
binding, add "!" syntax for the new binders which require parameters and not superclasses. Change backquotes for curly braces for user-given implicit arguments, following tradition. This requires a hack a la lpar-id-coloneq. Change ident to global for typeclass names in class binders. Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C t1 tn ]. Update affected theories. While hacking the parsing of { wf }, factorized the two versions of fix annotation parsing that were present in g_constr and g_vernac. Add the possibility of the user optionaly giving the priority for resolve and exact hints (used by type classes). Syntax not fixed yet: a natural after the list of lemmas in "Hint Resolve" syntax, a natural after a "|" after the instance constraint in Instance declarations (ex in Morphisms.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-06Toujours suite commits 10623 et 10624:herbelin
- l'occur-check doit être fait aussi quand on imite, - pour simplifier et en se basant sur les commentaires antérieurs à 1995 (de Chet?) et parlant de mimick_evar, on restreint l'appel à mimick_evar au cas où l'instance contient des Meta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10626 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-06Suite commit 10623:herbelin
- les erreurs de solve_simple_evar_eqn étaient rattrapées par mégarde, - à défaut de traitement des conv_pbs dans unification.ml, on évite d'accumuler des contraintes pour l'instant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10624 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-06Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nherbelin
dans certains cas. Branchement au passage de w_unify vers evar_conv et solve_simple_eqn en cas d'équations entre Evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-05Correction d'une typo restant du commit 10557 et cause d'échec de contribsherbelin
telles que Godel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10622 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-29Petite modif pour pouvoir faire "intros until 0" qui introduit autant aspiwack
que possible des variables qui ont déjà un nom joli tout plein. La conséquence c'est qu'on peut aussi faire "destruct 0" qui est vachement moins intéressant... Mais bon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10610 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Suspension de l'introduction de delta dans apply : certaines contribsherbelin
qui utilisent apply pour l'automatisation explosent (cf CatsInZFC qui passe de 20mn de compilation à 7h), d'autres instancient les métas par des expressions plus dépliées qu'avant, ce qui conduit à des échecs après coup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10571 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Added default canonical structures (see example in test-suite)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place d'une option "modulo_conv" pour contrôler l'usage de cette delta. - Pour éviter que rewrite ne réussise trop souvent, la delta est désactivée pour les tactiques d'élimination (une étude fine reste à faire). - On n'utilise aussi delta que sur les sous-termes du problème d'unification initial. C'est une heuristique qui est intuitive mais qui reste à être évaluée. - Au bilan, le surcoût en temps de compilation des theories est d'un peu moins d'1%. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Correction de ce qui semble être un petit bug dans la gestion de laherbelin
marge de manoeuvre vis a vis de eta dans l'unification : la convention est qu'on donne la forme eta-reduite avec l'indication du nombre d'expansions autorisées mais ce nombre était incorrect pour l'unification pattern de w_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10556 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-11Correction d'un bug de clearnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10552 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Fixing bug 1795 (occur check was not correctly done)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10551 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Solde de code mort et petites optimisations sur lesquels je suisherbelin
tombé au cours du temps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
eauto instead of an arbitrary tactic. Export more from eauto to allow easier debugging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Move generally useful definition of nf_evar on contexts to evarutil.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10532 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-07Mise en place d'une toute petite amélioration de l'unification deherbelin
apply : si on a trouvé une méta, alors, on l'utilise pour instancier les trous lors de la tentative de conversion modulo delta. Cela permet ainsi de résoudre de petits cas d'unification, tel que celui annoncé échouant dans le "beginner question" du 6 fevrier 2008 de coq-club. Solde au passage de modifs cosmétiques de setoid_replace.ml avant abandon probable du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Finish let| implementation and document itmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Debug 0-ary typeclasses support, use new redefinition support for default tacticmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10482 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-21Correction du bug #1754notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10458 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ↵msozeau
wrapper around Ltac program_simpl ::= . !!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18bug in accessing n-th abstractionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10451 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is ↵msozeau
backwards compatible. Update CHANGES with things i've done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-15Generalize instance declarations to any context, better name handling. Add ↵msozeau
hole kind info for topconstrs. Derive eta_expansion from functional extensionality axiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but ↵msozeau
implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ↵msozeau
evars and try to solve them too. Finally, rework tactics on setoids and design a saturating tactic to help solve goals on any setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10428 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-02Better resolution of implicit parameters in typeclass binders, add ↵msozeau
extensionality tactic to apply the axiom properly and fix test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
Variable, et plus de trucs useless qui traînaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
Au passage, un peu plus de standardisation des noms de fonctions de globalisation Principe de base : locate_foo : qualid -> foo (échoue avec Not_found) global : reference -> global_reference (échoue avec UserError) global_of_foo : foo -> global_reference (échoue avec UserError) f_with_alias : se comporte comme f mais prenant aussi en compte les notations de la forme "Notation id:=ref" Principale exception : locate, au lieu de locate_global locate_global_with_alias, qui prend en entrée un "qualid located" Restent beaucoup de fonctions qui pourraient utiliser global_with_alias au lieu de global, notamment dans contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12- Préservation des appels récursifs de tête dans ltac (réponse au "wish"herbelin
implicite du rapport de bug #468); utilisation pour cela d'un mécanisme différent de localisation des échecs Ltac (mécanisme probablement à affiner). - Factorisation au passage des appels au débuggeur Ltac. - Trivialités en passant dans clenv.ml. - Tentative de documentation de l'infâme Reductionops.instance et essai de déplacement plus amont du test "s = []". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10222 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12Uniformisation du comportement de rewrite et rewrite in : quand leherbelin
filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution uniforme permettant d'être conservatif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Amendement à la révision 10124 : déplacement de apprec_nohdbeta entreherbelin
is_fconv et le test d'équations simples (on admettra que is_fconv est a priori plus efficace pour réduire que nohdbeta -- et de fait, sur Stalmarck/algoRun, apprec_nohdbeta part en vrille alors que if_fconv réussit vite). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10159 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 08:08:11 +0000