aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/indfun.ml
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11990 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-18Désactivation de dumpglob lors des appels a functional induction (erreurs ↵notin
parasites du Lexer) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11706 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23first attempt to allow Function to deal with dependent pattern matching. ↵jforest
This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
for record fields (using "someproj : sometype where not := constr" syntax). Only one notation allowed currently and no redeclaration after the record declaration either (will be done for typeclasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-23Open notation for declaring record instances.msozeau
It solves feature request 1852, makes me and Arnaud happy and will permit to factor some more code in typeclasses. - Records are introduced using the syntax "{| x := t; y := foo |}" and "with" clauses are currently parsed but not yet supported in the elaboration. You are invited to suggest other syntaxes :) - Missing fields are turned into holes, extra fields cause an error message. The current implementation finds the type of the record at pretyping time, from the typing constraint alone (and just expects an inductive with one constructor). It is then impossible to use scope information to parse the bodies: that may be wrong. The other solution I see is using the fields to detect the type earlier, before internalisation of the bodies, but then we get in name clash hell. - In funind/contrib/interface I mostly put [assert false] everywhere to avoid warnings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-23Generalized implementation of generalization.msozeau
- New constr_expr construct [CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr] to generalize the free vars of the [constr_expr], binding these using [binding_kind] and making a lambda or a pi (or deciding from the scope) using [abstraction_kind option] (abstraction_kind = AbsLambda | AbsPi) - Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{ ... }" for implicit bindings (both "..(" and "_(" seem much more difficult to implement). Subject to discussion! A few examples added in a test-suite file. - Also add missing syntax for implicit/explicit combinations for _binders_: "{( )}" means implicit for the generalized (outer) vars, explicit for the (inner) variable itself. Subject to discussion as well :) - Factor much typeclass instance declaration code. We now just have to force generalization of the term after the : in instance declarations. One more step to using Instance for records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-04Évolutions diverses et variées.herbelin
- Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
- Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-08correction of bug 1829jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10766 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-15Adapt funind to the RLetPattern constructor.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10676 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
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-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-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-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
utilities from Util. Some additions in Util, and simplifications in various files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an ↵msozeau
obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest
correction bug 1442 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9710 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-09Retour r9310 en attendant mieuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9629 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Meilleur anglais (cf 9619)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-27Detection des paramettres pour les Functions bien fondeesjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9182 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-19Gestion des arguments implicites dans les Functions bien fondeesjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9152 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-18correction of bug #1220jforest
adding a "using" optional argument to Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9150 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-14mise en conformite des messages d'erreur de Function avec la doc.jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9136 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9081 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-11Bug corrections in Function.jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9065 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18Code cleaning in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9054 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18Code cleaning in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9053 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-13bug correction when defining graph of fixpoints/definitions not generated by ↵jforest
F unction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9050 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-10+functional inversion now takes the function to invert as an optional argument. jforest
+ Code cleaning un Function code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9036 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04- completely new version of "functional inversion" using inversion onjforest
inductive - bug correction in "Functional scheme" and "functional inversion": the function are now parsed as references and not indent - adding a zeta normalization function in rawtermops to zeta normalize graph constructions (not used for now) - Bug correction in generation of functional principle types (if an arguments of the function has a type which is a sort) - adding a new persistent table for functional induction informations (graph,...) - new save mechanism for functional induction principles (reuse of proofs when possible) - Minor bug correction in proof of principle. - Distinguishing building_principles (that is save them) and making then (just construct their proof term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-13ajout d'un argument with_clean a Indfun.functional_induction permettant de ↵jforest
choisir ou non de faire du menage dans les hypotheses engendrees. La tactique au niveau utilisateur fait toujours le menage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8954 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-13rearrangement du code: deplacement du code effectuant functionalcourtieu
induction vers indfun.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8952 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-22LetTuple are now supported in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8841 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05Correction in generate_graph (now handles fun _ => fix ....)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8794 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into ↵jforest
to files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8781 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Replacing "GenFixpoint" with "Function" and "mes" with "measure"jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8735 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24+ Handling "if" and cast in GenFixpoint jforest
+ Correcting a bug in recursives funcitons detection in GenFixpoint + Parially handling applied binders in funcitonal principles generation tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8725 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14Si un fixpoint a plusieurs arguments, mais un seul de type inductif, letouzey
ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-10+ Changing a little functional schemes types jforest
+ New tactic to prove functions schemes + Add a command "Generate graph for <functionname>" to generate automatiquelly the graph associated to a function (usefull only when the function has not been defined by GenFixpoint). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8694 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-20Adding "New Functional Scheme" jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8649 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-14+ Debugging and cleaning functional principle generation tacticjforest
+ New functional induction now calls induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8627 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:08:00 +0000