aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-12-19In_dec transparent (wish #902)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6483 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6481 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6479 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6477 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6475 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6473 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6471 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6469 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6467 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6465 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-10Hugo fixed a bug of refine, and it revealed a bug of functionalcoq
induction. Some metas were left in the type of metas of the term given to refine by functional induction. This commit fixes this bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6462 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6460 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6459 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification ↵herbelin
n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Correction du bug de build_initial_predicate a révèlé un autre bug dans ↵herbelin
expand_arg git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6457 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6454 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Amélioration message localisation constructions et modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6453 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Réactivation des tests output avec test aussi de la nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6452 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Ajout d'une version nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6451 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09MAJ avec les particularités de l'afficheur v7 de la V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6450 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Test d'affichage d'un Fix donné avec /nherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6449 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Fichier non traductible (référence à des objets invisibles ce qui ↵herbelin
empêche de traduire Locate) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6448 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Intégré à Implicit.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6447 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Ajout suffixe 8 pour test en nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6446 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Plus de statut spécial pour Remarkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6445 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09VOFILES aussi pour make dependherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6444 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Désactivation du test du printer arithmétique v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6442 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09travail sur les types extraitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6439 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Ajout bug do_restrict_hypherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6438 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6437 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Bugs dans la déclaration du type du terme filtré si non définiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6433 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Bug nom exceptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6432 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6430 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6429 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-07* added subst_evaluable_referencesacerdot
* the Unfold hints of auto/eauto now use evaluable_global_references in place of global_references git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6428 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Uniformisation du nom d'entrée openconstr en le nom du type open_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6426 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Erreur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6425 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Garder les cast semble décidément le meilleur moyen de rester synchrone ↵herbelin
avec l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6424 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Suppression des cast après avoir utiliser l'information de type (Tacinv ↵herbelin
envoie à refine des métas castées avec des métas ?!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6423 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Déplacement de la coercion vis à vis du but au niveau de Refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6422 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Relâchement obligation d'une contrainte de type sur les Hole en position ↵herbelin
terminale, pour plus grande généralité de understand_gen_tcc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Déplacement de la coercion vis à vis du but au niveau de Refine suite à ↵herbelin
changement de CastedOpenConstr en OpenConstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6419 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ↵herbelin
que de fonctions récursives même si l'une de ses fonctions n'a pas de meta); suppression gmm au passage suite commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6418 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Ajout bug #888herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Ajout bug #889herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06C'est trop compliqué de mettre à jour les types du metamap en passant sous ↵herbelin
les lieurs, plus simple de garder le type avec un cast (cf bug #889) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6415 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 09:44:37 +0000