aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2006-08-25two minor bug corrections in General Recursive Functions jforest
and one un structural Functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9084 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-22making otags working jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la ↵jforest
generation des graphes de Function + Correction d'un petit bug dans les lemmes d'inversions de Function + Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9069 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-15working on functional induction automation (tactic finduction andcourtieu
fauto, not documented yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9067 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-08-08In the old version, recursive functions cannot be declared inside a sectionbertot
when the termination argument is based on the fact that some relation is well-founded. The goal correspond to the proof that the relation is well-founded is cleared of all useless hypotheses and variables, including variables that maybe used in the intermediary lemma that gathers all the proofs that need to be done interactively. As a result, this intermediary lemma cannot be re-used to prove this goal. The message is: Error: No such section variable or assumption : A This message appears at the time the user send the Qed command. This is problem report #PR1202 submitted by X. Leroy. The correction is to use the list of input variables to the function as the list of variables that should be cleared from the context. The function tclUSER_if_not_mes needs to be modified. This function is also used in contrib/funind/functional_principles_proofs.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9064 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18Correction bug #1192notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9055 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-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵herbelin
romega_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9041 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-07Correction bug 1172 + correction en passant de la taille des paramètres de ↵herbelin
famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-06Suite remplacement VernacDebug par VernacSetOptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9023 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Use typing informations while defining graphs for Function. jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9014 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04functional inversion now takes a quatified hypothesis as first argumentjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9009 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04adding comments and cleaning code jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9003 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-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-29forgot a file jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8994 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-29bug correctionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8993 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Passage des graphes de Function dans Type jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Fix wrong order of existentials in eterm.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8984 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suite passage ident -> hyp dans syntaxe de 'replace with in'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8981 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Mutually structurally recursive defs and rec using measures added.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8968 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Wellfounded recursion using subtac working again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8966 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Progress in new wf def typing.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8965 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-16Ajout de tactiques expérimentales basée sur functional induction.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8962 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-06-12changed comments.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8949 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Bug suite déplacement Int.v dans ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8934 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09oups: il faut penser a fermer la porte en partant (d'un fixpoint)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8931 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
- qualification correcte des noms en Haskell - on imprime les types de toutes les fonctions en Haskell - en Ocaml, les appels recursifs d'une f : 'a truc doivent se faire avec les _meme_ parametres de types 'a. Exemple illegal: let rec f = function [] -> 0 | l -> f [l];; On met maintenant des Obj.magic en conséquence. En Haskell (avec typage fourni), ca passe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8930 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08reparation bug 1006letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8921 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Détection bug rawwit suitecorrection trou de typage create_argherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8919 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07functional induction can now be used with jforest
using <principle> with <bindings> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8911 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06this time it's good jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8904 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06Error in last commit jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8903 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06protecting an uncaught exception Not_found jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8901 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06+ ameliorating the tactic "functional induction"jforest
+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-02debut de reparation du test d'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8891 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
Also enclose traces with try with clauses to avoid detypinging anomalies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8889 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01bug in alpha-conversionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8888 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01reparation bug #1128letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8886 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:12:50 +0000