aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-12-19Insertion unification non seulement en tête mais à l'intérieur des motifs ↵herbelin
(permet p.ex. de traiter le motif (Some O)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2322 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-18the function Ctast.section_path was wrong. It performed two reversebertot
operations on lists, which was equivalent to doing nothing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2320 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Pour ocamlweb ...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2319 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Oubli d'un quoteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2318 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18On ne peut plus appliquer des arguments à une syntaxe primitiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2317 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18There remained traces of streams with the old syntax.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2316 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Add a new file in the files needed for the "coq-interface" binary: the filebertot
contrib/interface/blast.cmo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2315 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Add dependencies for two new files in contrib/interfacebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2314 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Integrating the Ltac language and the Blast tool into the interfacebertot
capabilities: The Ltac language is the language that makes it possible to define new tactics without using the ocaml language (already present in coq for a few months). The Blast tool is a tool that checks whether the goals could be solve automatically and proposes the proof trace to the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2313 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18affichage correct du type des inductifs et constructeurs en presencebarras
de parametres git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2312 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18typo de parenthèsage + suppression de string (= str maintenant)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2311 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18anti revolution culturelle: retour des arguments logiquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2310 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18ote les redondances des entetesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18coq-bugs #12: probleme de metamap resolubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2308 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2307 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18parsing des branches de Cases au niveau lconstr (au lieu de constr)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2306 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Grossière erreur de typageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2305 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Nettoyage exceptions liées au vieux Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Nettoyage exceptions liées au vieux Case; réparation du try with UserError ↵herbelin
mal nommé dans findtype git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2303 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-17probleme des Require dans les sectionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2301 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-17le save de Correctness faisant assert falsebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2300 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-16Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + ↵herbelin
suppression des @Coercion, @Local et @Local Coercion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2299 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2298 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2297 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13MAJ de la traduction en ast des variables de section en qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2296 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Contournement du problème des evars de type, typées par défaut dans Type ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2295 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Affichage NewInduction/NewDesctructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2294 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Contournement du problème des evars de type, typées par défaut dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2293 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13package Debian 7.1, correction pb compilation native sur certaines architecturescourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2292 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
2001-12-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2290 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11suppression de l'affichage des noeuds Change_evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2289 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2288 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11ajout du document sur la nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2287 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11document sur les propositions de nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2286 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11Mise en place de coercion dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2285 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11Test des coercions dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10correction de bugs concernant la gestion des modules. debranchement du test ↵letouzey
d'extraction sur les Reals en attendant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2282 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2281 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-07*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2280 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-07*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2279 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Majherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2278 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Parade contre effet indésirable du commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2277 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Affichage des '_' pour Introsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2276 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Amélioration nommage hypothèses NewInduction (et incompatibilités)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2275 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2274 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2273 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 07:42:54 +0000