aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2006-02-12Nettoyage Bool:herbelin
Suppression de bool_2, bool_4 et bool_5 très ad hoc Renommage des lemmes demorgan* qui n'énoncent en fait pas les lois de de Morgan Tentative partielle de renommage (un peu) plus uniforme Pour les Hint: - bool_5 de core remplacé en mettant exact diff_false_true dans core (un peu plus faible mais marche dans la pratique pour les contribs) - bool_2 remplacé par la transitivité sur bool (plus fort mais OK dans la pratique, et pas trop fort pour ne pas atteindre la force de trans_eq) - bool_4 apparemment pas utilisé - andb_false_elim, spécifique, apparemment pas utilisé, et supprimé comme hint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8031 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Unification max_case et max_case2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8030 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Unification min_case et min_case2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8029 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8027 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-11Commentaires et compatibilité coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8026 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8024 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-10induction now admits multiple induction arguments. The principle mustcoq
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
2006-02-10code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8022 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8020 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-09very minor bug correction and cleanningbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8019 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-09securing intros (we now use h_intro)bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8018 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-09Minor bugs fixesbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8017 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8015 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Changing Set to Type for iter.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8014 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08One can use a measure {mes f x} instead of a well-founded relation in ↵bertot
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
2006-02-08Julien:bertot
+ 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
2006-02-08Localisation des erreurs de sorte du prétypageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8011 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8010 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8009 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8007 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07oubli de code de debuggingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8006 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Messages nth brancheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8005 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Idem numbering of 'Unfold', 'simpl', ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8004 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Amélioration des messages d'erreurs de tacred; unfold considère maintenant leherbelin
prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Ajout pluralherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8002 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Mise en conformité de l'ordre des occurrences de pattern avec l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8000 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7998 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et ↵herbelin
Russell O'Connor (redondance Acc_iter et Fix_F) + uniformisation indentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06warning seulement si mode verboseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7996 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 09:11:48 +0000