aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-07-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5936 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5934 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5933 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5931 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Mise en place mécanisme de compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5930 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Mise en place mécanisme de compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5929 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Suppression quotifyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5922 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-16Suppression quotifyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5918 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Suppression compilation explication.ml4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5916 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis a vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5915 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Branchement sur Util.loc et abstraction vis a vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5912 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5911 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis a vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5910 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5906 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5905 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-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5901 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #780: compilation of several units in the same coqtop processbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5900 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #794: conv made in wrong envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5897 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #790: better error_not_cleanbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5896 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bugs #667 and #783 (mimick_evar and loc_table on large files)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5894 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5891 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-12MAJ techniqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5890 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5889 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Eta-expansion du predicat dans build_indrec (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5887 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Eta-expansion du predicat pas seulement pour make_case mais aussi pour ↵herbelin
build_indrec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5884 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ↵herbelin
(c'est au moment de la construction dans Indrec qu'il faut eta-expanser -cf bug #784) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5883 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5880 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5879 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5878 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-08added commands to idecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5870 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5869 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-07bypass w_Define when w_refine-ingcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5868 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5867 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5866 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-07-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5863 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5862 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-02syntax compatibility fixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5861 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5860 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5859 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5858 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-30instantiate entry: constr -> lconstrcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5856 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5855 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:47:27 +0000