aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2004-10-04un paquet de corrections de bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6175 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01The "Add Setoid" command now has a new argument "as name" that is usedsacerdot
to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
Thus it does not work for setoid relations and it can replace setoid_replace when the user wants to specify what the relation should be. To solve the problem this commit enables the syntax setoid_replace E1 with E2 using relation R ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29New syntaxsacerdot
"setoid_rewrite dir term generate side conditions constr_list" to specify a list of side conditions that must be a subset of the generated new goals. Used to disambiguate in case of multiple set of generated side conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27firstorder bugfix to cope with elim of sigma types with goal is of the wrong ↵corbinea
sort git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6141 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-12inclusion de meta_map dans evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08The innersort is now computed as the more precise sort between thesacerdot
synthesized innersort and the expected innersort. This closes a bug that allowed to export non well-typed* terms like the following one: ((fun (X : (T1 : CProp)) => (E : (T2 : Type))) : (T1 -> T2 : CProp)) * non well-typed according to the rules that consider CProp as a primitive sort. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6082 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08The code used to compare the synthesized and the expected type (if available)sacerdot
to decide whether a conversion should be generated (exporting both types). The comparison function used is Coq alpha conversion, that is also up to Casts. When it was successful, the only type that was kept was the synthesized one. In several CoRN theorems it happened that the expected type carried a few casts to make subterms of it be of type/sort CProp (instead of Type). These casts were forgot, and the innersort computed was imprecise. This partial fix consists in keeping the expected type. However, it may happen (at least in theory) that the casts to CProp are part of the synthesized type and not of the expected type. In this case they will be lost anyway. Properly fixing the problem would mean recur over the two alpha-convertible terms to add the casts from both sources. However, this operation is very expensive and I would prefer to avoid it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6081 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06reparation des Extract Constant avec Haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03Ported to the new implementation of setoid_*.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6050 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03The old implementation of (setoid_replace c1 with c2) used to replacesacerdot
either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation will not do it. Thus I am replacing every occurrence of (setoid_replace c1 with c2) with (setoid_replace c1 with c2 || setoid_replace c2 with c1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6047 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6033 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Setoid_replace.setoid_replace: last argument (that was supposed to besacerdot
always None) removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5969 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Show Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5967 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-22correction d'un bug de la tactique pour les semi setoid rings.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5965 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-19Protection des accès tableau car, sur Sparc-linux, cela engendre une erreur ↵herbelin
fatale d'ocaml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5958 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-18Abstraction vis a vis du type loc pour ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5951 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-14ajout des unsafeCoerce + 2 bugs haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5904 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08* <style>...</style> tag no longer generated for theory filessacerdot
(the HELM/MoWGLI stylesheets do not longer require it) * helm:helm_link added to each <a/> element whose href is an URI * the required <body/> element was not generated for theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5877 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08- recent changes to doubleTypeInference.ml (that introduced doublesacerdot
type inference for inferred types) undone. Previous performance restored. - bug in cic2acic (code that used to be dead fixed): the type of a sort was computed as the sort itself - CPropRetyping in cic2acic modified to handle correctly the sort Set in the two cases Predicative Set / Impredicative Set - CPropRetyping.get_type_of used in place of Retyping.get_type_of everywhere in cic2acic. This closes (again, but more efficiently) the bug about CProps erroneously recognized as Types in inferred types git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5875 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08Commit to perform double type inference also on inner types.sacerdot
* Motivation: the inner sorts computed for the inner types were computed by Coq itself. Thus Nijmegen's CProp was exported as Type. To export CProp as CProp I have to implement a CProp-aware single type inference. To avoid the reimplementation I use double type inference. * Known problems: the double type inference algorithm is slower than the usual type inference algorithm. Moreover too many types and sorts are computed in this way. As a consequence the exportation module is now much slower (the exportation time seems to be doubled in the average case). In the future I will try to restore the original performances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5872 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-05Constants just after a "Let id : t. ... Qed" local variable declaration weresacerdot
exported as a copy of the variable id. Fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5865 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30updated printing of evar context (may loop ?)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29License de contrib/interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5849 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28contrib/interface *$*$@!corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5844 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau ↵letouzey
mind_record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5836 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-26Licence changed from GPL to Lesser GPL.sacerdot
DTDs licence is still GPL. This should create no problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5828 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25eq and eqT are the samebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5825 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-28Retour sur amendement de l'interprétation mult sur nat (bug 743) car ↵herbelin
incompatible avec la sémantique précédente qui identifiait "Z_of_nat x * Z_of_nat y" avec "Z_of_nat (x * y)" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5774 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-13"comments only" commit.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5744 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-07Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est ↵herbelin
de toutes façons inutile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5733 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21pb install de pcoqbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5695 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Copyright notice of files in contrib/xml made uniform.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Old file. The new version of this script is no longer distributed withsacerdot
Coq (the latest verion can be retrieved from the HELM and MoWGLI pages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5658 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07- theoryobject.dtd is the DTD for .theory filessacerdot
- copyright notice inserted in every DTD git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5657 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Loic code to pretty-print the generated proof-tree debranched (since itsacerdot
generates not well-formed XML files). An hook is left in xmlcommand.ml to register a pretty-printer function once a fixed implementation is provided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07CoRN CProp detection improved: products of "sort" CProp are now recognizedsacerdot
(they used to be exported as products of sort Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5652 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;sacerdot
^ ... ^ special verbatim code also backtracked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5651 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-06Fake dependent products in inductive definition types are no longer replacedsacerdot
with non dependent products. The main motivation is that inductive definition parameters often occurs as non-dependent products in the product types, but the binder names are still necessary to render the definition in the usual Coq way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5646 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-06Important bug fix: since coqdoc is now quoting XML reserved characters insacerdot
HTML tags (i.e. # ... #), strong verbatim tags must be now used (i.e. ^ ... ^). WARNING: it requires the fortcoming commit on coqdoc to work properly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5644 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-05Since coqdoc produces (X)HTML, HTML character entities can be usedsacerdot
in .v files. The exportation module produces generic XML ==> the character entities that were verbatim copied were never declared and the generated files were not well-formed XML files. Fixed by adding to the internal subset of the DTD an inclusion to the three files were the (X)HTML entities are defined. Due to technical reasons (HELM Getter URL rewriting), the chosen URL refers to the HELM web site. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5636 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-05correction rapide du bug PR\#592letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5635 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:20:55 +0000