aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Collapse)Author
2002-07-11Protection contre l'encapsulage de FailError dans Exc_located (sinon, par ↵herbelin
exemple, 'Try Tauto' ne marche pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2855 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-14Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2786 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Bug non vérification non redondance par Cutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2784 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Déplacement de proofs vers tacticsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2732 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichier des expressions de tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2714 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-27Ajout de Eval, Inst et Checkdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
gauche à droite des hypothèses dans Intuition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2696 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2693 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15Contournement de la fermeture ML dans VContextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2691 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
- Protection des "Match Context" contre les exceptions non UserError ni Fail - Remplacement des fermetures ML dans VTactic et VFTactic par des expressions de tactiques pour permettre l'intégration de Tactic Definition dans les états - Changement en conséquence de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2685 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14modification de clenv_merge:barras
on ajoute en premier lieu les contraintes concernant le terme puis apres celles concernant le type de chaque instantiation, au lieu d'alterner l'ajout de contraintes de terme et de type. A l'essai. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2682 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17typed unification in the case of Patternbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2654 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12backtrack unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2642 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12q: Commande introuvable.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2640 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2634 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10backtrack dans l'algo d'unificationbarras
fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Simplification des Clear internes dégénérés (sans hypothèses à effacer)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2626 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-03transformation des evar en meta preserve la linearite des metasbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2605 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-03changement de l'undo limitbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2604 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-27Simplification de Proof_type.prim_ruleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21backtrack de l'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2562 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-20encore quelques petites modif de l'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2553 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-18Rétablissement de look_for_interpdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2540 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-12Retablissement de interp_tab + injection id -> constr sans goaldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2527 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-12Propagation du pb de conversion dans clenv_unifyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2526 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-08renommage de fonctionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2521 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-07Clear ne substitue plus le corps dans le reste du butbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2517 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05unification faite de gauche a droite (et non pas l'inverse) pour eviter quebarras
clenv_typed_unify plante trop facilement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2511 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2509 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Uniformisation convert_hypherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2502 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Generalisation de l'utilisation de l'unification d'ordre 2barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2498 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22suppression de pop_namedbarras
meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2490 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12petite modif pour ne pas expanser trop de let pendant l'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2471 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-08prterm -> prterm_envfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20Convertibilité au lieu d'alpha-équivalence pour les motifs non linéaires ↵herbelin
de Match Context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2357 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19reparation de make doc (ocamlweb & _)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2321 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-17Mauvais nom d'erreur d'échec de nthherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2302 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 18:25:00 +0000