aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Collapse)Author
2000-01-28documentationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@284 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration ↵herbelin
du let-in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Renommage command en constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14bug mk_clenv_from lorsque pas d argumentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@252 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13mise a jour de refiner.ml (reports de modifs de la V6.3)barras
bug possible dans lib.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@250 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13 - états fabriqués avec -silentfilliatr
- compilation theories avec -q - correction but de tclORELSE qui doit maintenant rattraper aussi TypeError et RefinerError git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@249 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13 - méthode load sur les Hintsfilliatr
- CAST pris en compte dans Astterm - Coercin.lookup_path_to_sort_from protégé par un try/with git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10 - erreurs Pretypefilliatr
- Write / Restore State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10debug resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-09 - constantes avec recettesfilliatr
- discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-08deplacement de Discharge dans toplevelfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-05premier debugagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03 - coqmktopfilliatr
- #use "include.ml";; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@198 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03modules profile, Coqinit et Coqtop (=main)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03 - global_reference traite des variablesfilliatr
- construct_reference, avec environnement en argument - link de Class - Definition et Check au toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@193 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02modifs pour premiere edition de liensfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02Pfedit (fin)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@188 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01poursuite de Vernacentriesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01module Pfeditfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@169 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - environment -> safe_environmentfilliatr
- unsafe_env -> env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01 - Typing -> Safe_typingfilliatr
- proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-29portage modules Evarconv et Evarutilfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@161 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-25typage des existentielles dans Typing_ev; suppression metamap inutiles dans ↵filliatr
typage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@141 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-25Backtrack sur modif Evd.evd_conclherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@139 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24MAJ pour fusion avec pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Vernacinterp et Vernacentries (partiellement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@133 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-22module Wcclausenvfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@130 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-22module Tactics (debut)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@129 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-19module Pattern, Wcclausenv (interface) et Tacticalsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-22module Macros et Tacinterpfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@115 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-22 - module Redinfo dans library/ pour les constantes d'éliminationfilliatr
- module Tacred : fonctions de reductions utilisees dans les tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@114 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-20 - documentation repertoire proofs/filliatr
- IsAppL of constr * constr list ==> répercussion - module Clenv (suite; as terminé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-20module Clenv (debut)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@111 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-20modules Evar_refiner et Typing_evfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-19module Refinerfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@109 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-19les variables existentielles contiennent maintenant un environnement (typefilliatr
unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres le module Environ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@108 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-18mise en place module Refinerfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@107 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr
toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument supplémentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-14module Logicfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-14module Proof_treesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-13 - re-introduction d'une evar_map dans unsafe_envfilliatr
- les var. ex. sont des entiers, et non plus des section_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@99 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-13redeplacement des var. ex. dans kernel :-)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@97 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-08module Logic (ne compile pas encore)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@95 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-08deplacement des var. ex. dans proofsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@94 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 15:07:16 +0000