aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-02-28*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8103 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8101 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-27quelques raccourcis commodes + un f_equal plus efficaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8100 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-27dp: sortie Whyfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8099 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8097 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8095 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-25changement de path du site webnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8094 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-25ajoute un warning sur htmlppnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8093 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8091 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8088 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23trying to fix a bug in pazrameter order in the multiple inductioncoq
tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8087 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Ajout 'exists! x:A, P (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8086 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Ajout 'exists! x:A, Pherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8083 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22Minimum pour documentation TeX de la biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8082 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22Work on recursive definitionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8080 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22Add vernacular file for subtaccoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8079 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8078 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22Julien:bertot
+ 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
2006-02-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8074 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-21Work with binder lists, problem of tyconscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-21Latest fixes, should work fine now for non recursive definitions, although ↵coq
still has some syntax problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8072 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8070 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Fix minor bugcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8069 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Forgot a filecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8068 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Monday work, working with coercions and implicit argscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8067 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Forgot another file...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8066 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Forgot one filecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8065 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Change in subtac modulescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8064 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-20Rewrite of the subtac tactic, needs some work on implicit arguments.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8063 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8061 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8059 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8057 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17bug correctionbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8056 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17Julien:bertot
+ 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
2006-02-17cleaningcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8054 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17bug correction in the decomposition of an induction scheme.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8053 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17changed the decomposition of an induction schemecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8052 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8050 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-16added isProd to term.mli.coq
added elim_scheme to tactics.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8049 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8047 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-15continuing the generalization of "induction". Now induction schemescoq
with multiple args AND no main induction arg can be used directly with induction. The last functional argument is not necessary anymore. For example: nat_double_ind: forall R : nat -> nat -> Prop, ...branches... -> forall n m : nat, R n m. is ok. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8046 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8044 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8042 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-13Bug correction in saving proofs: If a hook opens a proof but does not close ↵bertot
it then the delete_current_proof () does not delete the good proof if executed AFTER the hook. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8041 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-13firstorder fails gracefullly when encountering untypable higher-order termscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8040 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8036 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Bug Scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8034 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Zmax et Zminmaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8033 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 05:22:52 +0000