aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* bug : import -> export dans RequireGravatar filliatr1999-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@260 85f007b7-540e-0410-9357-904b9bb8a0f7
* message erreur SchemeGravatar herbelin1999-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
| | | | | | | | | 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
* Les inductifs dans Scheme doivent être des ident d'inductifsGravatar herbelin1999-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@256 85f007b7-540e-0410-9357-904b9bb8a0f7
* - états fabriqués avec -silentGravatar filliatr1999-12-13
| | | | | | | | | - 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
* - méthode load sur les HintsGravatar filliatr1999-12-13
| | | | | | | | - 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
* petite erreur dans CommandGravatar filliatr1999-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@246 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation interfacesGravatar filliatr1999-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@244 85f007b7-540e-0410-9357-904b9bb8a0f7
* modulesGravatar filliatr1999-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
* - erreurs PretypeGravatar filliatr1999-12-10
| | | | | | | - Write / Restore State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7
* debug resetGravatar filliatr1999-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@228 85f007b7-540e-0410-9357-904b9bb8a0f7
* debug discharge et inductifsGravatar filliatr1999-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
* - constantes avec recettesGravatar filliatr1999-12-09
| | | | | | | | - 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
* Discharge (encore bugge)Gravatar filliatr1999-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@223 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
* initialisation load path (provisoire)Gravatar filliatr1999-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@214 85f007b7-540e-0410-9357-904b9bb8a0f7
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
* erreurs lexicalesGravatar filliatr1999-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@211 85f007b7-540e-0410-9357-904b9bb8a0f7
* premier debugageGravatar filliatr1999-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation nativeGravatar filliatr1999-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug make_strength repareGravatar filliatr1999-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@200 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coqmktopGravatar filliatr1999-12-03
| | | | | | | - #use "include.ml";; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@198 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
* - global_reference traite des variablesGravatar filliatr1999-12-03
| | | | | | | | | - 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
* Modifs suite à intégration de class.mlGravatar herbelin1999-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version initialeGravatar herbelin1999-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@191 85f007b7-540e-0410-9357-904b9bb8a0f7
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
* module CommandGravatar filliatr1999-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
* module MetasyntaxGravatar filliatr1999-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@177 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@175 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage Vernacentries (debut)Gravatar filliatr1999-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@173 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Typing -> Safe_typingGravatar filliatr1999-12-01
| | | | | | | | | - 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
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@161 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7
* On se fait la main: plus de precision si ill-formed rec bodyGravatar herbelin1999-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@119 85f007b7-540e-0410-9357-904b9bb8a0f7
* module LogicGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement des var. ex. dans proofsGravatar filliatr1999-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@94 85f007b7-540e-0410-9357-904b9bb8a0f7
* with_heavy_rollback deplace dans StatesGravatar filliatr1999-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@89 85f007b7-540e-0410-9357-904b9bb8a0f7
* corrections pour ocamlwebGravatar filliatr1999-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@88 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement du toplevelGravatar filliatr1999-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@83 85f007b7-540e-0410-9357-904b9bb8a0f7
* module DeclareGravatar filliatr1999-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
| | | | | | | | | - module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@73 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation repertoire toplevelGravatar filliatr1999-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@72 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 12:59:02 +0000