aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Collapse)AuthorAge
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Test files for subtac.Gravatar msozeau2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the proof of principlesGravatar jforest2006-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for new unification, not used in default version as it really changes ↵Gravatar msozeau2006-04-10
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8695 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Changing a little functional schemes types Gravatar jforest2006-04-10
| | | | | | | | | | | | + 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
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun ↵Gravatar msozeau2006-04-10
| | | | | | | | | | | (previous and current version work). Changed the type of typing constraints so as to have all the necessary information on abstract tycons. Updates of subtac to use the new type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
| | | | | | | | | | - Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
* appel Zenon sans preludeGravatar filliatr2006-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8664 85f007b7-540e-0410-9357-904b9bb8a0f7
* utilisation de la VM pour la normalisation finale de romegaGravatar letouzey2006-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8660 85f007b7-540e-0410-9357-904b9bb8a0f7
* correctifs de bug pour romega: Gravatar letouzey2006-03-23
| | | | | | | | | | | | | | | | | | | | | | | | 1) dans refl_omega, on donnait a OmegaSolver un generateur de numero d'equations new_eq_id qui pouvait clasher avec les numeros d'equations initiaux créés avec new_omega_id. => on sépare en deux compteurs, un pour les equations omegas, l'autre pour les variables omegas. On en profite pour reinitialiser ces compteurs à chaque session romega, histoire que romega devienne reproductible. 2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti à un endroit. ATTENTION: ceci peut changer le comportement d'omega. Surveiller le resultat du prochain bench nocturne. 3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication dans une hypothese lors du recalcul final. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac fixes, single fixpoint definitions are working again. Added a toggle ↵Gravatar msozeau2006-03-22
| | | | | | | | | | on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made pretyping a functor over a coercion implementation. Pretyping.Default ↵Gravatar msozeau2006-03-22
| | | | | | | | | | | uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
| | | | | | | | | | | destruct x y z using scheme + replace c1 with c2 <in hyp> has now a new optional argument <as tac> replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding "New Functional Scheme" Gravatar jforest2006-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8649 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning dead code Gravatar jforest2006-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8637 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Debugging and cleaning functional principle generation tacticGravatar jforest2006-03-14
| | | | | | | | | + New functional induction now calls induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
* -Debugging multiple induction, a bug appeared when having functionGravatar courtieu2006-03-12
| | | | | | | | | | arguments to a principle (like in map_ind). -Added nbranches and npredicates to elim_scheme, and made the elimc field optional. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8622 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleaning Gravatar jforest2006-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain ↵Gravatar jforest2006-03-07
| | | | | | is_empty in those versions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exploitation du 'let rec' + présentationGravatar herbelin2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8134 85f007b7-540e-0410-9357-904b9bb8a0f7
* New files for subtacGravatar coq2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8133 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactic haRVey pour appeler haRVey (contrib/dp)Gravatar filliatr2006-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8107 85f007b7-540e-0410-9357-904b9bb8a0f7
* appel de ZenonGravatar filliatr2006-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8106 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar filliatr2006-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8103 85f007b7-540e-0410-9357-904b9bb8a0f7
* dp: sortie WhyGravatar filliatr2006-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on recursive definitionsGravatar coq2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add vernacular file for subtacGravatar coq2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Julien:Gravatar bertot2006-02-22
| | | | | | | | + Induction principle for general recursion + Bug correction in structural principles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8076 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work with binder lists, problem of tyconsGravatar coq2006-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Latest fixes, should work fine now for non recursive definitions, although ↵Gravatar coq2006-02-21
| | | | | | still has some syntax problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix minor bugGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a fileGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monday work, working with coercions and implicit argsGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot another file...Gravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot one fileGravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8063 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug correctionGravatar bertot2006-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Julien:Gravatar bertot2006-02-17
| | | | | | | | | + Compatibility with new induction + Induction principle for general recursion preparation still continuing + Cleaning dead code ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8055 85f007b7-540e-0410-9357-904b9bb8a0f7
* changed the decomposition of an induction schemeGravatar coq2006-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8052 85f007b7-540e-0410-9357-904b9bb8a0f7
* firstorder fails gracefullly when encountering untypable higher-order termsGravatar corbinea2006-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8040 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
| | | | | | | | | | | | | be explicitely given, and ALL parameters and args of the scheme must be given (only branches must be omitted). For the moment, only principle like generated by GenFixpoint (functional induction) are usable. That is the predicate must have a additional paramter like in: (P x1 ... xn (f p1...pm x1...xn)) Example of use : induction x y (add x y) using add_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
* very minor bug correction and cleanningGravatar bertot2006-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8019 85f007b7-540e-0410-9357-904b9bb8a0f7
* securing intros (we now use h_intro)Gravatar bertot2006-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor bugs fixesGravatar bertot2006-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing Set to Type for iter.Gravatar bertot2006-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8014 85f007b7-540e-0410-9357-904b9bb8a0f7
* One can use a measure {mes f x} instead of a well-founded relation in ↵Gravatar bertot2006-02-08
| | | | | | | | | GenFixpoint. If the function takes only one argument, it can be deleted from the wf/mes part. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Julien:Gravatar bertot2006-02-08
| | | | | | | | | + Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment. + Bug correction in new functional induction + For now no induction principle for general recursive definition is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8012 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 21:19:58 +0000