diff options
71 files changed, 410 insertions, 1176 deletions
diff --git a/dev/doc/about-hints b/dev/doc/about-hints deleted file mode 100644 index 95712c3cf9..0000000000 --- a/dev/doc/about-hints +++ /dev/null @@ -1,454 +0,0 @@ -An investigation of how ZArith lemmas could be classified in different -automation classes - -- Reversible lemmas relating operators (to be declared as hints but - needing precedences) -- Equivalent notions (one has to be considered as primitive and the - other rewritten into the canonical one) -- Isomorphisms between structure (one structure has to be considered - as more primitive than the other for a give operator) -- Irreversible simplifications (to be declared with precedences) -- Reversible bottom-up simplifications (to be used in hypotheses) -- Irreversible bottom-up simplifications (to be used in hypotheses - with precedences) -- Rewriting rules (relevant for autorewrite, or for an improved auto) - -Note: this analysis, made in 2001, was previously stored in -theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating -the standard library. - -(**********************************************************************) -(** * Reversible lemmas relating operators *) -(** Probably to be declared as hints but need to define precedences *) - -(** ** Conversion between comparisons/predicates and arithmetic operators *) - -(** Lemmas ending by eq *) -(** -<< -Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` -Zabs_eq: (x:Z)`0 <= x`->`|x| = x` -Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` -Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` -Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` -Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` -Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` -Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` -Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` -Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` -Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` ->> -*) - -(** ** Conversion between nat comparisons and Z comparisons *) - -(** Lemmas ending by eq *) -(** -<< -inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)` ->> -*) - -(** Lemmas ending by Zge *) -(** -<< -inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` ->> -*) - -(** ** Conversion between comparisons *) - -(** Lemmas ending by Zge *) -(** -<< -not_Zlt: (x,y:Z)~`x < y`->`x >= y` -Zle_ge: (m,n:Z)`m <= n`->`n >= m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` -not_Zle: (x,y:Z)~`x <= y`->`x > y` -Zlt_gt: (m,n:Z)`m < n`->`n > m` -Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -not_Zge: (x,y:Z)~`x >= y`->`x < y` -Zgt_lt: (m,n:Z)`m > n`->`n < m` -Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` -not_Zgt: (x,y:Z)~`x > y`->`x <= y` -Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` -Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` -Zge_le: (m,n:Z)`m >= n`->`n <= m` -Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` -Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` -Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` -Zle_refl: (n,m:Z)`n = m`->`n <= m` ->> -*) - -(** ** Irreversible simplification involving several comparaisons *) -(** useful with clear precedences *) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` -Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` ->> -*) - -(** ** What is decreasing here ? *) - -(** Lemmas ending by eq *) -(** -<< -Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` ->> -*) - -(**********************************************************************) -(** * Useful Bottom-up lemmas *) - -(** ** Bottom-up simplification: should be used *) - -(** Lemmas ending by eq *) -(** -<< -Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` -Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` -Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` -Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` -Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` -Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` -Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` -Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` ->> -*) - -(** Lemmas ending by Zle *) -(** << Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` -Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` -Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *) - -(** ** Bottom-up irreversible (syntactic) simplification *) - -(** Lemmas ending by Zle *) -(** -<< -Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` ->> -*) - -(** ** Other unclearly simplifying lemmas *) - -(** Lemmas ending by Zeq *) -(** -<< -Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` ->> -*) - -(* Lemmas ending by Zgt *) -(** -<< -Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` ->> -*) - -(* Lemmas ending by Zlt *) -(** -<< -pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` ->> -*) - -(* Lemmas ending by Zle *) -(** -<< -Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` -OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y` ->> -*) - - -(**********************************************************************) -(** * Irreversible lemmas with meta-variables *) -(** To be used by EAuto *) - -(* Hints Immediate *) -(** Lemmas ending by eq *) -(** -<< -Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m` ->> -*) - -(** Lemmas ending by Zge *) -(** -<< -Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` -Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` -Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` -Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` -Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` -Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p` ->> -*) - - -(**********************************************************************) -(** * Unclear or too specific lemmas *) -(** Not to be used ? *) - -(** ** Irreversible and too specific (not enough regular) *) - -(** Lemmas ending by Zle *) -(** -<< -Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` -Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` -OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` -OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t` ->> -*) - -(** ** Expansion and too specific ? *) - -(** Lemmas ending by Zge *) -(** -<< -Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` -Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` -Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y` ->> -*) - -(** ** Reversible but too specific ? *) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_minus: (n,m:Z)`0 < m`->`n-m < n` ->> -*) - -(**********************************************************************) -(** * Lemmas to be used as rewrite rules *) -(** but can also be used as hints *) - -(** Left-to-right simplification lemmas (a symbol disappears) *) - -(** -<< -Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) -Zmin_n_n: (n:Z)`(Zmin n n) = n` -Zmult_1_n: (n:Z)`1*n = n` -Zmult_n_1: (n:Z)`n*1 = n` -Zminus_plus: (n,m:Z)`n+m-n = m` -Zle_plus_minus: (n,m:Z)`n+(m-n) = m` -Zopp_Zopp: (x:Z)`(-(-x)) = x` -Zero_left: (x:Z)`0+x = x` -Zero_right: (x:Z)`x+0 = x` -Zplus_inverse_r: (x:Z)`x+(-x) = 0` -Zplus_inverse_l: (x:Z)`(-x)+x = 0` -Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` -Zmult_one: (x:Z)`1*x = x` -Zero_mult_left: (x:Z)`0*x = 0` -Zero_mult_right: (x:Z)`x*0 = 0` -Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y` ->> -*) - -(** Right-to-left simplification lemmas (a symbol disappears) *) - -(** -<< -Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` -Zs_pred: (n:Z)`n = (Zs (Zpred n))` -Zplus_n_O: (n:Z)`n = n+0` -Zmult_n_O: (n:Z)`0 = n*0` -Zminus_n_O: (n:Z)`n = n-0` -Zminus_n_n: (n:Z)`0 = n-n` -Zred_factor6: (x:Z)`x = x+0` -Zred_factor0: (x:Z)`x = x*1` ->> -*) - -(** Unclear orientation (no symbol disappears) *) - -(** -<< -Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` -Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` -Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` -Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` -Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` -Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` -Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` -Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` -Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` -Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` -Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` -Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` -Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` -Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` -Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` -Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` -Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` -Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` -Zplus_sym: (x,y:Z)`x+y = y+x` -Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` -Zmult_sym: (x,y:Z)`x*y = y*x` -Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` -Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` -Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` -Zopp_one: (x:Z)`(-x) = x*(-1)` -Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` -Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` -Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` -Zred_factor1: (x:Z)`x+x = x*2` -Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` -Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` -Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` -Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` -Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n` ->> -*) - -(** nat <-> Z *) -(** -<< -inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` -inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` -inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` -inj_minus1: - (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` -inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0` ->> -*) - -(** Too specific ? *) -(** -<< -Zred_factor5: (x,y:Z)`x*0+y = y` ->> -*) diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd deleted file mode 100644 index cc33efd483..0000000000 --- a/dev/doc/cic.dtd +++ /dev/null @@ -1,231 +0,0 @@ -<?xml encoding="ISO-8859-1"?> - -<!-- DTD FOR CIC OBJECTS: --> - -<!-- CIC term declaration --> - -<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST| - LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'> - -<!-- CIC sorts --> - -<!ENTITY % sort '(Prop|Set|Type)'> - -<!-- CIC sequents --> - -<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> - -<!-- CIC objects: --> - -<!ELEMENT ConstantType %term;> -<!ATTLIST ConstantType - name CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT ConstantBody %term;> -<!ATTLIST ConstantBody - for CDATA #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT CurrentProof (Conjecture*,body)> -<!ATTLIST CurrentProof - of CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT InductiveDefinition (InductiveType+)> -<!ATTLIST InductiveDefinition - noParams NMTOKEN #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Variable (body?,type)> -<!ATTLIST Variable - name CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Sequent %sequent;> -<!ATTLIST Sequent - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!-- Elements used in CIC objects, which are not terms: --> - -<!ELEMENT InductiveType (arity,Constructor*)> -<!ATTLIST InductiveType - name CDATA #REQUIRED - inductive (true|false) #REQUIRED> - -<!ELEMENT Conjecture %sequent;> -<!ATTLIST Conjecture - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Constructor %term;> -<!ATTLIST Constructor - name CDATA #REQUIRED> - -<!ELEMENT Decl %term;> -<!ATTLIST Decl - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Def %term;> -<!ATTLIST Def - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Hidden EMPTY> -<!ATTLIST Hidden - id ID #REQUIRED> - -<!ELEMENT Goal %term;> - -<!-- CIC terms: --> - -<!ELEMENT LAMBDA (decl*,target)> -<!ATTLIST LAMBDA - sort %sort; #REQUIRED> - -<!ELEMENT LETIN (def*,target)> -<!ATTLIST LETIN - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT PROD (decl*,target)> -<!ATTLIST PROD - type %sort; #REQUIRED> - -<!ELEMENT CAST (term,type)> -<!ATTLIST CAST - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT REL EMPTY> -<!ATTLIST REL - value NMTOKEN #REQUIRED - binder CDATA #REQUIRED - id ID #REQUIRED - idref IDREF #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT SORT EMPTY> -<!ATTLIST SORT - value CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT APPLY (%term;)+> -<!ATTLIST APPLY - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT VAR EMPTY> -<!ATTLIST VAR - relUri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- The substitutions are ordered by increasing de Bruijn --> -<!-- index. An empty substitution means that that index is --> -<!-- not accessible. --> -<!ELEMENT META (substitution*)> -<!ATTLIST META - no NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT IMPLICIT EMPTY> -<!ATTLIST IMPLICIT - id ID #REQUIRED> - -<!ELEMENT CONST EMPTY> -<!ATTLIST CONST - uri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTIND EMPTY> -<!ATTLIST MUTIND - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT MUTCONSTRUCT EMPTY> -<!ATTLIST MUTCONSTRUCT - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - noConstr NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)> -<!ATTLIST MUTCASE - uriType CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT FIX (FixFunction+)> -<!ATTLIST FIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT COFIX (CofixFunction+)> -<!ATTLIST COFIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- Elements used in CIC terms: --> - -<!ELEMENT FixFunction (type,body)> -<!ATTLIST FixFunction - name CDATA #REQUIRED - recIndex NMTOKEN #REQUIRED> - -<!ELEMENT CofixFunction (type,body)> -<!ATTLIST CofixFunction - name CDATA #REQUIRED> - -<!ELEMENT substitution ((%term;)?)> - -<!-- Explicit named substitutions: --> - -<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)> -<!ATTLIST instantiate - id ID #IMPLIED> - -<!-- Sintactic sugar for CIC terms and for CIC objects: --> - -<!ELEMENT arg %term;> -<!ATTLIST arg - relUri CDATA #REQUIRED> - -<!ELEMENT decl %term;> -<!ATTLIST decl - id ID #REQUIRED - type %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT def %term;> -<!ATTLIST def - id ID #REQUIRED - sort %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT target %term;> - -<!ELEMENT term %term;> - -<!ELEMENT type %term;> - -<!ELEMENT arity %term;> - -<!ELEMENT patternsType %term;> - -<!ELEMENT inductiveTerm %term;> - -<!ELEMENT pattern %term;> - -<!ELEMENT body %term;> diff --git a/dev/doc/minicoq.tex b/dev/doc/minicoq.tex deleted file mode 100644 index a34b03a491..0000000000 --- a/dev/doc/minicoq.tex +++ /dev/null @@ -1,98 +0,0 @@ -\documentclass{article} - -\usepackage{fullpage} -\input{./macros.tex} -\newcommand{\minicoq}{\textsf{minicoq}} -\newcommand{\nonterm}[1]{\textit{#1}} -\newcommand{\terminal}[1]{\textsf{#1}} -\newcommand{\listzero}{\textit{LIST$_0$}} -\newcommand{\listun}{\textit{LIST$_1$}} -\newcommand{\sep}{\textit{SEP}} - -\title{Minicoq: a type-checker for the pure \\ - Calculus of Inductive Constructions} - - -\begin{document} - -\maketitle - -\section{Introduction} - -\minicoq\ is a minimal toplevel for the \Coq\ kernel. - - -\section{Grammar of terms} - -The grammar of \minicoq's terms is given in Figure~\ref{fig:terms}. - -\begin{figure}[htbp] - \hrulefill - \begin{center} - \begin{tabular}{lrl} - term & ::= & identifier \\ - & $|$ & \terminal{Rel} integer \\ - & $|$ & \terminal{Set} \\ - & $|$ & \terminal{Prop} \\ - & $|$ & \terminal{Type} \\ - & $|$ & \terminal{Const} identifier \\ - & $|$ & \terminal{Ind} identifier integer \\ - & $|$ & \terminal{Construct} identifier integer integer \\ - & $|$ & \terminal{[} name \terminal{:} term - \terminal{]} term \\ - & $|$ & \terminal{(} name \terminal{:} term - \terminal{)} term \\ - & $|$ & term \verb!->! term \\ - & $|$ & \terminal{(} \listun\ term \terminal{)} \\ - & $|$ & \terminal{(} term \terminal{::} term \terminal{)} \\ - & $|$ & \verb!<! term \verb!>! \terminal{Case} - term \terminal{of} \listzero\ term \terminal{end} - \\[1em] - name & ::= & \verb!_! \\ - & $|$ & identifier - \end{tabular} - \end{center} - \hrulefill - \caption{Grammar of terms} - \label{fig:terms} -\end{figure} - -\section{Commands} -The grammar of \minicoq's commands are given in -Figure~\ref{fig:commands}. All commands end with a dot. - -\begin{figure}[htbp] - \hrulefill - \begin{center} - \begin{tabular}{lrl} - command & ::= & \terminal{Definition} identifier \terminal{:=} term. \\ - & $|$ & \terminal{Definition} identifier \terminal{:} term - \terminal{:=} term. \\ - & $|$ & \terminal{Parameter} identifier \terminal{:} term. \\ - & $|$ & \terminal{Variable} identifier \terminal{:} term. \\ - & $|$ & \terminal{Inductive} \terminal{[} \listzero\ param - \terminal{]} \listun\ inductive \sep\ - \terminal{with}. \\ - & $|$ & \terminal{Check} term. - \\[1em] - param & ::= & identifier - \\[1em] - inductive & ::= & identifier \terminal{:} term \terminal{:=} - \listzero\ constructor \sep\ \terminal{$|$} - \\[1em] - constructor & ::= & identifier \terminal{:} term - \end{tabular} - \end{center} - \hrulefill - \caption{Commands} - \label{fig:commands} -\end{figure} - - -\end{document} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/dev/doc/transition-V5.10-V6 b/dev/doc/transition-V5.10-V6 deleted file mode 100644 index df7b65dd8b..0000000000 --- a/dev/doc/transition-V5.10-V6 +++ /dev/null @@ -1,5 +0,0 @@ -The V5.10 archive has been created with cvs in February 1995 by -Jean-Christophe Filliâtre. It was moved to archive V6 in March 1996. -At this occasion, the contrib directory (user-contributions) were -moved to a separate directory and some theories (like ALGEBRA) moved -to the user-contributions directory too. diff --git a/dev/doc/transition-V6-V7 b/dev/doc/transition-V6-V7 deleted file mode 100644 index e477c9ff9d..0000000000 --- a/dev/doc/transition-V6-V7 +++ /dev/null @@ -1,8 +0,0 @@ -The V6 archive has been created in March 1996 with files from the -former V5.10 archive and has been abandoned in 2000. - -A new archive named V7 has been created in August 1999 by -Jean-Christophe Filliâtre with a new architecture placing the -type-checking at the kernel of Coq. This new architecture came with a -"cleaner" organization of files, a uniform indentation style, uniform -headers, etc. diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4287702b3a..b90a53220d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -20,13 +20,12 @@ open Univ open Environ open Printer open Constr -open Goptions open Genarg open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true -let _ = set_bool_option_value ["Printing";"Matching"] false +let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) diff --git a/engine/namegen.ml b/engine/namegen.ml index db72dc8ec3..0f346edd3e 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -210,7 +210,7 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = let mangle_names = ref false -let _ = Goptions.( +let () = Goptions.( declare_bool_option { optdepr = false; optname = "mangle auto-generated names"; @@ -226,7 +226,7 @@ let set_mangle_names_mode x = begin mangle_names := true end -let _ = Goptions.( +let () = Goptions.( declare_string_option { optdepr = false; optname = "mangled names prefix"; diff --git a/engine/uState.ml b/engine/uState.ml index 5b0671c06e..6aecc368e6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -577,25 +577,33 @@ let add_global_univ uctx u = uctx_universes = univs } let make_flexible_variable ctx ~algebraic u = - let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if algebraic then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - let has_upper_constraint () = - Univ.Constraint.exists - (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u) - (Univ.ContextSet.constraints cstrs) - in - if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ()) - then Univ.LSet.add u avars else avars - else avars - in - {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'} + let open Univ in + let {uctx_local = cstrs; uctx_univ_variables = uvars; + uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in + assert (try LMap.find u uvars == None with Not_found -> true); + match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with + | Some v -> + let uvars' = LMap.add u (Some (Universe.make v)) uvars in + { ctx with uctx_univ_variables = uvars'; } + | None -> + let uvars' = LMap.add u None uvars in + let avars' = + if algebraic then + let uu = Universe.make u in + let substu_not_alg u' v = + Option.cata (fun vu -> Universe.equal uu vu && not (LSet.mem u' avars)) false v + in + let has_upper_constraint () = + Constraint.exists + (fun (l,d,r) -> d == Lt && Level.equal l u) + (ContextSet.constraints cstrs) + in + if not (LMap.exists substu_not_alg uvars || has_upper_constraint ()) + then LSet.add u avars else avars + else avars + in + {ctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = avars'} let make_nonalgebraic_variable ctx u = { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } diff --git a/engine/univMinim.ml b/engine/univMinim.ml index f10e6d2ec1..68c2724f26 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -15,7 +15,7 @@ open UnivSubst let set_minimization = ref true let is_set_minimization () = !set_minimization -let _ = +let () = Goptions.(declare_bool_option { optdepr = false; optname = "minimization to Set"; diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d5f0b7bff6..07ed7825ff 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -605,13 +605,13 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function (str "This expression should be coercible to a pattern.")) c let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "no parameters in constructors"; + optkey = ["Asymmetric";"Patterns"]; + optread = (fun () -> !asymmetric_patterns); + optwrite = (fun a -> asymmetric_patterns:=a); +}) (** Local universe and constraint declarations. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 70ce6cef19..0f5fa14c23 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -195,7 +195,7 @@ let without_specific_symbols l = (* Set Record Printing flag *) let record_print = ref true -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index fe07a1c90e..afdc8f1511 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -868,6 +868,21 @@ let constraints_for ~kept g = let domain g = LMap.domain g.entries +let choose p g u = + let exception Found of Level.t in + let ru = (repr g u).univ in + if p ru then Some ru + else + try LMap.iter (fun v -> function + | Canonical _ -> () (* we already tried [p ru] *) + | Equiv v' -> + let rv = (repr g v').univ in + if rv == ru && p v then raise (Found v) + (* NB: we could also try [p v'] but it will come up in the + rest of the iteration regardless. *) + ) g.entries; None + with Found v -> Some v + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index a389b35993..4dbfac5c73 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -73,6 +73,10 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option +(** [choose p g u] picks a universe verifying [p] and equal + to [u] in [g]. *) + (** [constraints_for ~kept g] returns the constraints about the universes [kept] in [g] up to transitivity. diff --git a/library/goptions.ml b/library/goptions.ml index 154b863fa1..bb9b4e29fc 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -276,10 +276,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) let cread () = cast (read ()) in let cwrite l v = warn (); change l OptSet (uncast v) in let cappend l v = warn (); change l OptAppend (uncast v) in - value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab; - write - -type 'a write_function = 'a -> unit + value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab let declare_int_option = declare_option diff --git a/library/goptions.mli b/library/goptions.mli index 3d7df18fed..900217e06b 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -122,16 +122,14 @@ type 'a option_sig = { (** The [preprocess] function is triggered before setting the option. It can be used to emit a warning on certain values, and clean-up the final value. *) -type 'a write_function = 'a -> unit - val declare_int_option : ?preprocess:(int option -> int option) -> - int option option_sig -> int option write_function + int option option_sig -> unit val declare_bool_option : ?preprocess:(bool -> bool) -> - bool option_sig -> bool write_function + bool option_sig -> unit val declare_string_option: ?preprocess:(string -> string) -> - string option_sig -> string write_function + string option_sig -> unit val declare_stringopt_option: ?preprocess:(string option -> string option) -> - string option option_sig -> string option write_function + string option option_sig -> unit (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index a6f432b5bd..575d964158 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -33,7 +33,7 @@ let print_constr t = let debug x = if !cc_verbose then Feedback.msg_debug (x ()) -let _= +let () = let gdopt= { optdepr=false; optname="Congruence Verbose"; @@ -61,7 +61,7 @@ module ST=struct type t = {toterm: int IntPairTable.t; tosign: (int * int) IntTable.t} - let empty ()= + let empty () = {toterm=IntPairTable.create init_size; tosign=IntTable.create init_size} @@ -321,7 +321,7 @@ let compress_path uf i j = uf.map.(j).cpath<-i let rec find_aux uf visited i= let j = uf.map.(i).cpath in - if j<0 then let _ = List.iter (compress_path uf i) visited in i else + if j<0 then let () = List.iter (compress_path uf i) visited in i else find_aux uf (i::visited) j let find uf i= find_aux uf [] i diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f6eea3c5c4..16890ea260 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -500,7 +500,7 @@ let info_file f = let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in - let _ = declare_bool_option + let () = declare_bool_option {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; @@ -572,14 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n let optims () = !opt_flag_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} -let _ = declare_int_option +let () = declare_int_option { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; @@ -593,7 +593,7 @@ let _ = declare_int_option let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; @@ -605,7 +605,7 @@ let _ = declare_bool_option let file_comment_ref = ref "" let file_comment () = !file_comment_ref -let _ = declare_string_option +let () = declare_string_option {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index a212d13453..37fc81ee38 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -33,7 +33,7 @@ DECLARE PLUGIN "ground_plugin" let ground_depth=ref 3 -let _= +let ()= let gdopt= { optdepr=false; optname="Firstorder Depth"; @@ -47,7 +47,7 @@ let _= declare_int_option gdopt -let _= +let ()= let congruence_depth=ref 100 in let gdopt= { optdepr=true; (* noop *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b68b34ca35..c864bfe9f7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -375,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig = optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) } -let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true @@ -388,7 +388,7 @@ let function_debug_sig = optwrite = (fun b -> function_debug := b) } -let _ = declare_bool_option function_debug_sig +let () = declare_bool_option function_debug_sig let do_observe () = !function_debug @@ -406,7 +406,7 @@ let strict_tcc_sig = optwrite = (fun b -> strict_tcc := b) } -let _ = declare_bool_option strict_tcc_sig +let () = declare_bool_option strict_tcc_sig exception Building_graph of exn diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 338839ee96..d9b19c1ae6 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -373,7 +373,7 @@ open Libnames let print_info_trace = ref None -let _ = declare_int_option { +let () = declare_int_option { optdepr = false; optname = "print info trace"; optkey = ["Info" ; "Level"]; diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 3eb049dbab..ae4b53325f 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -446,7 +446,7 @@ let do_print_results_at_close () = let _ = Declaremods.append_end_library_hook do_print_results_at_close -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cb3a0aaed9..c4d8072ba5 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2039,7 +2039,7 @@ let _ = let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -2048,7 +2048,7 @@ let _ = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 877d4ee758..99b9e881f6 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -89,7 +89,7 @@ let batch = ref false open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Ltac batch debug"; diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 561bfc5d7c..19256e054d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -65,7 +65,7 @@ let assoc_flags ist : tauto_flags = let negation_unfolding = ref true open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "unfolding of not in intuition"; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 402e8b91e6..d4bafe773f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -51,7 +51,7 @@ let get_lra_option () = -let _ = +let () = let int_opt l vref = { @@ -89,11 +89,11 @@ let _ = optwrite = (fun x -> Certificate.dump_file := x) } in - let _ = declare_bool_option solver_opt in - let _ = declare_stringopt_option dump_file_opt in - let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in - let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in - let _ = declare_bool_option lia_enum_opt in + let () = declare_bool_option solver_opt in + let () = declare_stringopt_option dump_file_opt in + let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in + let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in + let () = declare_bool_option lia_enum_opt in () diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d8adb17710..dff25b3a42 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -64,7 +64,7 @@ let write f x = f:=x open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega system time displaying flag"; @@ -72,7 +72,7 @@ let _ = optread = read display_system_flag; optwrite = write display_system_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega action display flag"; @@ -80,7 +80,7 @@ let _ = optread = read display_action_flag; optwrite = write display_action_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega old style flag"; @@ -88,7 +88,7 @@ let _ = optread = read old_style_flag; optwrite = write old_style_flag } -let _ = +let () = declare_bool_option { optdepr = true; optname = "Omega automatic reset of generated names"; @@ -96,7 +96,7 @@ let _ = optread = read reset_flag; optwrite = write reset_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega takes advantage of context variables with body"; diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3de5923968..aab1e47555 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -54,7 +54,7 @@ let opt_pruning= optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} -let _ = declare_bool_option opt_pruning +let () = declare_bool_option opt_pruning type form= Atom of int diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 840a05e02b..e66fa10d5b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -236,7 +236,7 @@ let opt_verbose= optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} -let _ = declare_bool_option opt_verbose +let () = declare_bool_option opt_verbose let check = ref false @@ -247,7 +247,7 @@ let opt_check= optread=(fun () -> !check); optwrite=(fun b -> check:=b)} -let _ = declare_bool_option opt_check +let () = declare_bool_option opt_check open Pp @@ -255,7 +255,7 @@ let rtauto_tac gls= Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; let gamma={next=1;env=[]} in let gl=pf_concl gls in - let _= + let () = if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in @@ -267,7 +267,7 @@ let rtauto_tac gls= | Tactic_debug.DebugOn 0 -> Search.debug_depth_first | _ -> Search.depth_first in - let _ = + let () = begin reset_info (); if !verbose then @@ -279,7 +279,7 @@ let rtauto_tac gls= with Not_found -> user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); @@ -287,7 +287,7 @@ let rtauto_tac gls= Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in - let _ = step_count := 0; node_count := 0 in + let () = step_count := 0; node_count := 0 in let main = mkApp (force node_count l_Reflect, [|build_env gamma; build_form formula; @@ -295,7 +295,7 @@ let rtauto_tac gls= let term= applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ @@ -314,7 +314,7 @@ let rtauto_tac gls= else Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in - let _ = + let () = if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then Feedback.msg_info (str "Internal tactic executed in " ++ diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 22475fef34..490e8fbdbc 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -32,13 +32,13 @@ open Tacticals open Tacmach let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect 1.3 compatibility flag"; - Goptions.optkey = ["SsrOldRewriteGoalsOrder"]; - Goptions.optread = (fun _ -> !ssroldreworder); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssroldreworder := b) } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect 1.3 compatibility flag"; + optkey = ["SsrOldRewriteGoalsOrder"]; + optread = (fun _ -> !ssroldreworder); + optdepr = false; + optwrite = (fun b -> ssroldreworder := b) }) (** The "simpl" tactic *) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f67cf20e49..8cebe62e16 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -66,14 +66,14 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let _ = - Goptions.declare_bool_option - { Goptions.optname = "have type classes"; - Goptions.optkey = ["SsrHave";"NoTCResolution"]; - Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); - } +let () = + Goptions.(declare_bool_option + { optname = "have type classes"; + optkey = ["SsrHave";"NoTCResolution"]; + optread = (fun _ -> !ssrhaveNOtcresolution); + optdepr = false; + optwrite = (fun b -> ssrhaveNOtcresolution := b); + }) open Constrexpr diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 2dff0cc84f..b48030b963 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1605,14 +1605,14 @@ let old_tac = V82.tactic let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect identifiers"; - Goptions.optkey = ["SsrIdents"]; - Goptions.optdepr = false; - Goptions.optread = (fun _ -> !ssr_reserved_ids); - Goptions.optwrite = (fun b -> ssr_reserved_ids := b) - } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect identifiers"; + optkey = ["SsrIdents"]; + optdepr = false; + optread = (fun _ -> !ssr_reserved_ids); + optwrite = (fun b -> ssr_reserved_ids := b) + }) let is_ssr_reserved s = let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_' @@ -2355,13 +2355,13 @@ END let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect rewrite"; - Goptions.optkey = ["SsrRewrite"]; - Goptions.optread = (fun _ -> !ssr_rw_syntax); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssr_rw_syntax := b) } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect rewrite"; + optkey = ["SsrRewrite"]; + optread = (fun _ -> !ssr_rw_syntax); + optdepr = false; + optwrite = (fun b -> ssr_rw_syntax := b) }) let lbrace = Char.chr 123 (** Workaround to a limitation of coqpp *) diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 824666ba9c..8bf4816e99 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -119,13 +119,13 @@ and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat (* 0 cost pp function. Active only if Debug Ssreflect is Set *) let ppdebug_ref = ref (fun _ -> ()) let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect debugging"; - Goptions.optkey = ["Debug";"Ssreflect"]; - Goptions.optdepr = false; - Goptions.optread = (fun _ -> !ppdebug_ref == ssr_pp); - Goptions.optwrite = (fun b -> +let () = + Goptions.(declare_bool_option + { optname = "ssreflect debugging"; + optkey = ["Debug";"Ssreflect"]; + optdepr = false; + optread = (fun _ -> !ppdebug_ref == ssr_pp); + optwrite = (fun b -> Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) } + if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) let ppdebug s = !ppdebug_ref s diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 5061aeff88..7104b8586e 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -184,13 +184,13 @@ let cofixp_reducible flgs _ stk = false let debug_cbv = ref false -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "cbv visited constants display"; - Goptions.optkey = ["Debug";"Cbv"]; - Goptions.optread = (fun () -> !debug_cbv); - Goptions.optwrite = (fun a -> debug_cbv:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "cbv visited constants display"; + optkey = ["Debug";"Cbv"]; + optread = (fun () -> !debug_cbv); + optwrite = (fun a -> debug_cbv:=a); +}) let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 2c2a8fe49e..1edcc499f0 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -401,7 +401,7 @@ let add_class cl = let automatically_import_coercions = ref false open Goptions -let _ = +let () = declare_bool_option { optdepr = true; (* remove in 8.8 *) optname = "automatic import of coercions"; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e21c2fda85..30eb70d0e7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -35,7 +35,7 @@ open Globnames let use_typeclasses_for_conversion = ref true -let _ = +let () = Goptions.(declare_bool_option { optdepr = false; optname = "use typeclass resolution during conversion"; @@ -183,7 +183,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) with UnableToUnify _ -> let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in - let _ = + let () = try evdref := the_conv_x_leq env eqT eqT' !evdref with UnableToUnify _ -> raise NoSubtacCoercion in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 072ac9deed..33ced6d6e0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -138,7 +138,7 @@ open Goptions let wildcard_value = ref true let force_wildcard () = !wildcard_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; @@ -148,7 +148,7 @@ let _ = declare_bool_option let synth_type_value = ref true let synthetize_type () = !synth_type_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; @@ -158,7 +158,7 @@ let _ = declare_bool_option let reverse_matching_value = ref true let reverse_matching () = !reverse_matching_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; @@ -168,7 +168,7 @@ let _ = declare_bool_option let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; @@ -178,7 +178,7 @@ let _ = declare_bool_option let print_primproj_compatibility_value = ref false let print_primproj_compatibility () = !print_primproj_compatibility_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "backwards-compatible printing of primitive projections"; optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; @@ -257,8 +257,7 @@ let lookup_index_as_renamed env sigma t n = let print_factorize_match_patterns = ref true -let _ = - let open Goptions in +let () = declare_bool_option { optdepr = false; optname = "factorization of \"match\" patterns in printing"; @@ -268,8 +267,7 @@ let _ = let print_allow_match_default_clause = ref true -let _ = - let open Goptions in +let () = declare_bool_option { optdepr = false; optname = "possible use of \"match\" default pattern in printing"; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f370ad7ae2..6c268de3b3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -33,14 +33,14 @@ type unify_fun = TransparentState.t -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result let debug_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Print states sent to Evarconv unification"; - Goptions.optkey = ["Debug";"Unification"]; - Goptions.optread = (fun () -> !debug_unification); - Goptions.optwrite = (fun a -> debug_unification:=a); -} + optkey = ["Debug";"Unification"]; + optread = (fun () -> !debug_unification); + optwrite = (fun a -> debug_unification:=a); +}) (*******************************************) (* Functions to deal with impossible cases *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index abf52d2893..3391750209 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -108,7 +108,7 @@ let search_guard ?loc env possible_indexes fixdefs = let strict_universe_declarations = ref true let is_strict_universe_declarations () = !strict_universe_declarations -let _ = +let () = Goptions.(declare_bool_option { optdepr = false; optname = "strict universe declaration"; diff --git a/pretyping/program.ml b/pretyping/program.ml index bbabbefdc3..7e38c09189 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -75,7 +75,7 @@ let is_program_cases () = !program_cases open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "preferred transparency of Program obligations"; @@ -83,7 +83,7 @@ let _ = optread = get_proofs_transparency; optwrite = set_proofs_transparency; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "program cases"; @@ -91,7 +91,7 @@ let _ = optread = (fun () -> !program_cases); optwrite = (:=) program_cases } -let _ = +let () = declare_bool_option { optdepr = false; optname = "program generalized coercion"; diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e632976ae5..a57ee6e292 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,14 +29,14 @@ exception Elimconst their parameters in its stack. *) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Generate weak constraints between Irrelevant universes"; - Goptions.optkey = ["Cumulativity";"Weak";"Constraints"]; - Goptions.optread = (fun () -> not !UState.drop_weak_constraints); - Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a); -} + optkey = ["Cumulativity";"Weak";"Constraints"]; + optread = (fun () -> not !UState.drop_weak_constraints); + optwrite = (fun a -> UState.drop_weak_constraints:=not a); +}) (** Support for reduction effects *) @@ -830,14 +830,14 @@ let fix_recarg ((recindices,bodynum),_) stack = *) let debug_RAKAM = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Print states of the Reductionops abstract machine"; - Goptions.optkey = ["Debug";"RAKAM"]; - Goptions.optread = (fun () -> !debug_RAKAM); - Goptions.optwrite = (fun a -> debug_RAKAM:=a); -} + optkey = ["Debug";"RAKAM"]; + optread = (fun () -> !debug_RAKAM); + optwrite = (fun a -> debug_RAKAM:=a); +}) let equal_stacks sigma (x, l) (y, l') = let f_equal x y = eq_constr sigma x y in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4aea2c3db9..c68890a87f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -37,7 +37,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "check that typeclasses proof search returns unique solutions"; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8c1aae26ae..094fcd923e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -43,25 +43,25 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "Unification is keyed"; - Goptions.optkey = ["Keyed";"Unification"]; - Goptions.optread = (fun () -> !keyed_unification); - Goptions.optwrite = (fun a -> keyed_unification:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Unification is keyed"; + optkey = ["Keyed";"Unification"]; + optread = (fun () -> !keyed_unification); + optwrite = (fun a -> keyed_unification:=a); +}) let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Print states sent to tactic unification"; - Goptions.optkey = ["Debug";"Tactic";"Unification"]; - Goptions.optread = (fun () -> !debug_unification); - Goptions.optwrite = (fun a -> debug_unification:=a); -} + optkey = ["Debug";"Tactic";"Unification"]; + optread = (fun () -> !debug_unification); + optwrite = (fun a -> debug_unification:=a); +}) (** Making this unification algorithm correct w.r.t. the evar-map abstraction breaks too much stuff. So we redefine incorrect functions here. *) diff --git a/printing/printer.ml b/printing/printer.ml index 94b514239a..2bbda279bd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -34,7 +34,7 @@ let should_unfoc() = !enable_unfocused_goal_printing let should_gname() = !enable_goal_names_printing -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -45,7 +45,7 @@ let _ = (* This is set on by proofgeneral proof-tree mode. But may be used for other purposes *) -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -55,7 +55,7 @@ let _ = optwrite = (fun b -> enable_goal_tags_printing:=b) } -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -140,7 +140,7 @@ let pr_cases_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) -let _ = Termops.Internal.set_print_constr +let () = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t)) let pr_in_comment x = str "(* " ++ x ++ str " *)" @@ -431,7 +431,7 @@ let pr_context_limit_compact ?n env sigma = (* If [None], no limit *) let print_hyps_limit = ref (None : int option) -let _ = +let () = let open Goptions in declare_int_option { optdepr = false; @@ -639,7 +639,7 @@ let print_evar_constraints gl sigma = let should_print_dependent_evars = ref false -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/printing/printmod.ml b/printing/printmod.ml index 1360ad4af4..a8d7b0c1a8 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -41,7 +41,7 @@ type short = OnlyNames | WithContents let short = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "short module printing"; diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index cc1bcc66ae..3e2093db4a 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -52,7 +52,7 @@ let write_diffs_option = function | "removed" -> diff_option := `REMOVED | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".") -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "show diffs in proofs"; diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index 65a94a2c60..cef3fd3f5e 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -53,7 +53,7 @@ let parse_goal_selector = function with Failure _ -> CErrors.user_err Pp.(str err_msg) end -let _ = let open Goptions in +let () = let open Goptions in declare_string_option { optdepr = false; optname = "default goal selector" ; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 647e87150b..886a62cb89 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -16,18 +16,18 @@ open Environ open Evd let use_unification_heuristics_ref = ref true -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "Solve unification constraints at every \".\""; - Goptions.optkey = ["Solve";"Unification";"Constraints"]; - Goptions.optread = (fun () -> !use_unification_heuristics_ref); - Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Solve unification constraints at every \".\""; + optkey = ["Solve";"Unification";"Constraints"]; + optread = (fun () -> !use_unification_heuristics_ref); + optwrite = (fun a -> use_unification_heuristics_ref:=a); +}) let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index ed8df29d7b..2ca4f0afb4 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -176,7 +176,7 @@ end (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "bullet behavior"; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index af97d40579..095aa36f03 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -53,7 +53,7 @@ let default_proof_mode = ref (find_proof_mode "No") let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; @@ -128,13 +128,13 @@ let push a l = l := a::!l; update_proof_mode () exception NoSuchProof -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -272,12 +272,12 @@ let get_used_variables () = (cur_pstate ()).section_vars let get_universe_decl () = (cur_pstate ()).universe_decl let proof_using_auto_clear = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Proof using Clear Unused"; - Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; - Goptions.optread = (fun () -> !proof_using_auto_clear); - Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } +let () = Goptions.(declare_bool_option + { optdepr = false; + optname = "Proof using Clear Unused"; + optkey = ["Proof";"Using";"Clear";"Unused"]; + optread = (fun () -> !proof_using_auto_clear); + optwrite = (fun b -> proof_using_auto_clear := b) }) let set_used_variables l = let open Context.Named.Declaration in @@ -490,7 +490,7 @@ let update_global_env () = (p, ()))) (* XXX: Bullet hook, should be really moved elsewhere *) -let _ = +let () = let hook n = try let prf = give_me_the_proof () in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 0981584bb5..6658c37f41 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -54,14 +54,14 @@ let strong_cbn flags = strong_with_flags whd_cbn flags let simplIsCbn = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Plug the simpl tactic to the new cbn mechanism"; - Goptions.optkey = ["SimplIsCbn"]; - Goptions.optread = (fun () -> !simplIsCbn); - Goptions.optwrite = (fun a -> simplIsCbn:=a); -} + optkey = ["SimplIsCbn"]; + optread = (fun () -> !simplIsCbn); + optwrite = (fun a -> simplIsCbn:=a); +}) let set_strategy_one ref l = let k = diff --git a/stm/stm.ml b/stm/stm.ml index 3324df3066..c078dbae56 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -44,7 +44,6 @@ module AsyncOpts = struct async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; @@ -61,7 +60,6 @@ module AsyncOpts = struct async_proofs_mode = APoff; async_proofs_private_flags = None; - async_proofs_full = false; async_proofs_never_reopen_branch = false; async_proofs_tac_error_resilience = `Only [ "curly" ]; @@ -1442,11 +1440,14 @@ end = struct (* {{{ *) let perspective = ref [] let set_perspective l = perspective := l + let is_inside_perspective st = true + (* This code is now disabled. If an IDE needs this feature, make it accessible again. + List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st + *) + let task_match age t = match age, t with - | Fresh, BuildProof { t_states } -> - not !cur_opt.async_proofs_full || - List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states + | Fresh, BuildProof { t_states } -> is_inside_perspective t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1482,8 +1483,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !cur_opt.async_proofs_full || t_drop - then `Stay(t_states,[States t_states]) + if t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> @@ -2126,8 +2126,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch - let init () = queue := Some (TaskQueue.create - (if !cur_opt.async_proofs_full then 1 else 0)) + let init () = queue := Some (TaskQueue.create 0) end (* }}} *) @@ -2150,7 +2149,6 @@ let async_policy () = let delegate name = get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !cur_opt.async_proofs_full let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); @@ -2257,8 +2255,7 @@ let collect_proof keep cur hd brkind id = else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc - else if (is_vtkeep keep) && - (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) + else if (is_vtkeep keep) && (not(State.is_cached_and_valid id)) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2646,13 +2643,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = name by looking at the load path! *) List.iter Mltop.add_coq_path iload_path; + Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; + begin match doc_type with | Interactive ln -> let dp = match ln with | TopLogical dp -> dp | TopPhysical f -> dirpath_of_file f in - Safe_typing.allow_delayed_constants := true; Declaremods.start_library dp | VoDoc f -> @@ -2663,7 +2661,6 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = set_compilation_hints f | VioDoc f -> - Safe_typing.allow_delayed_constants := true; let ldir = dirpath_of_file f in check_coq_overwriting ldir; let () = Flags.verbosely Declaremods.start_library ldir in @@ -2842,12 +2839,12 @@ let process_back_meta_command ~newtip ~head oid aast w = Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok let allow_nested_proofs = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Nested Proofs Allowed"; - Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; - Goptions.optread = (fun () -> !allow_nested_proofs); - Goptions.optwrite = (fun b -> allow_nested_proofs := b) } +let () = Goptions.(declare_bool_option + { optdepr = false; + optname = "Nested Proofs Allowed"; + optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; + optread = (fun () -> !allow_nested_proofs); + optwrite = (fun b -> allow_nested_proofs := b) }) let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = @@ -2869,11 +2866,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtQuery, w -> let id = VCS.new_node ~id:newtip () in let queue = - if !cur_opt.async_proofs_full then `QueryQueue (ref false) - else if VCS.is_vio_doc () && - VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) - then `SkipQueue + if VCS.is_vio_doc () && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque (Vernacprop.under_control x.expr) + then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -3206,8 +3202,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !cur_opt.async_proofs_full then - Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try diff --git a/stm/stm.mli b/stm/stm.mli index 0c0e19ce5c..b6071fa56b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -16,7 +16,9 @@ open Names module AsyncOpts : sig type cache = Force - type async_proofs = APoff | APonLazy | APon + type async_proofs = APoff + | APonLazy (* Delays proof checking, but does it in master *) + | APon type tac_error_filter = [ `None | `Only of string list | `All ] type stm_opt = { @@ -27,7 +29,6 @@ module AsyncOpts : sig async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; diff --git a/tactics/auto.ml b/tactics/auto.ml index 81e487b77d..441fb68acc 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -172,15 +172,14 @@ let global_info_trivial = ref false let global_info_auto = ref false let add_option ls refe = - let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = String.concat " " ls; - Goptions.optkey = ls; - Goptions.optread = (fun () -> !refe); - Goptions.optwrite = (:=) refe } - in () - -let _ = + Goptions.(declare_bool_option + { optdepr = false; + optname = String.concat " " ls; + optkey = ls; + optread = (fun () -> !refe); + optwrite = (:=) refe }) + +let () = add_option ["Debug";"Trivial"] global_debug_trivial; add_option ["Debug";"Auto"] global_debug_auto; add_option ["Info";"Trivial"] global_info_trivial; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 5959dd54b1..719d552def 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -80,7 +80,7 @@ let get_typeclasses_depth () = !typeclasses_depth open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "do typeclass search avoiding eta-expansions " ^ @@ -89,7 +89,7 @@ let _ = optread = get_typeclasses_limit_intros; optwrite = set_typeclasses_limit_intros; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "during typeclass resolution, solve instances according to their dependency order"; @@ -97,7 +97,7 @@ let _ = optread = get_typeclasses_dependency_order; optwrite = set_typeclasses_dependency_order; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "use iterative deepening strategy"; @@ -105,7 +105,7 @@ let _ = optread = get_typeclasses_iterative_deepening; optwrite = set_typeclasses_iterative_deepening; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "compat"; @@ -113,7 +113,7 @@ let _ = optread = get_typeclasses_filtered_unification; optwrite = set_typeclasses_filtered_unification; } -let set_typeclasses_debug = +let () = declare_bool_option { optdepr = false; optname = "debug output for typeclasses proof search"; @@ -121,7 +121,7 @@ let set_typeclasses_debug = optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "debug output for typeclasses proof search"; @@ -129,7 +129,7 @@ let _ = optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } -let _ = +let () = declare_int_option { optdepr = false; optname = "verbosity of debug output for typeclasses proof search"; @@ -137,7 +137,7 @@ let _ = optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } -let set_typeclasses_depth = +let () = declare_int_option { optdepr = false; optname = "depth for typeclasses proof search"; @@ -1126,7 +1126,7 @@ let solve_inst env evd filter unique split fail = end in sigma -let _ = +let () = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = @@ -1151,7 +1151,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = end in (sigma, term) -let _ = +let () = Hook.set Typeclasses.solve_one_instance_hook (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index b8adb792e8..3019fc0231 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -329,21 +329,21 @@ module Search = Explore.Make(SearchProblem) let global_debug_eauto = ref false let global_info_eauto = ref false -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Debug Eauto"; - Goptions.optkey = ["Debug";"Eauto"]; - Goptions.optread = (fun () -> !global_debug_eauto); - Goptions.optwrite = (:=) global_debug_eauto } - -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Info Eauto"; - Goptions.optkey = ["Info";"Eauto"]; - Goptions.optread = (fun () -> !global_info_eauto); - Goptions.optwrite = (:=) global_info_eauto } +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "Debug Eauto"; + optkey = ["Debug";"Eauto"]; + optread = (fun () -> !global_debug_eauto); + optwrite = (:=) global_debug_eauto }) + +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "Info Eauto"; + optkey = ["Info";"Eauto"]; + optread = (fun () -> !global_info_eauto); + optwrite = (:=) global_info_eauto }) let mk_eauto_dbg d = if d == Debug || !global_debug_eauto then Debug diff --git a/tactics/equality.ml b/tactics/equality.ml index b8967775bf..bdc95941b2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -69,7 +69,7 @@ let use_injection_in_context = function | None -> !injection_in_context | Some flags -> flags.injection_in_context -let _ = +let () = declare_bool_option { optdepr = false; optname = "injection in context"; @@ -714,7 +714,7 @@ exception DiscrFound of let keep_proof_equalities_for_injection = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "injection on prop arguments"; @@ -1501,7 +1501,7 @@ let intro_decomp_eq tac data (c, t) = decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl end -let _ = declare_intro_decomp_eq intro_decomp_eq +let () = declare_intro_decomp_eq intro_decomp_eq (* [subst_tuple_term dep_pair B] @@ -1666,7 +1666,7 @@ user = raise user error specific to rewrite let regular_subst_tactic = ref true -let _ = +let () = declare_bool_option { optdepr = false; optname = "more regular behavior of tactic subst"; @@ -1911,8 +1911,8 @@ let replace_term dir_opt c = (* Declare rewriting tactic for intro patterns "<-" and "->" *) -let _ = +let () = let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in Hook.set Tactics.general_rewrite_clause gmr -let _ = Hook.set Tactics.subst_one subst_one +let () = Hook.set Tactics.subst_one subst_one diff --git a/tactics/hints.ml b/tactics/hints.ml index e64e08dbde..77479f9efa 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -194,14 +194,14 @@ let write_warn_hint = function | "Strict" -> warn_hint := `STRICT | _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") -let _ = - Goptions.declare_string_option - { Goptions.optdepr = false; - Goptions.optname = "behavior of non-imported hints"; - Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; - Goptions.optread = read_warn_hint; - Goptions.optwrite = write_warn_hint; - } +let () = + Goptions.(declare_string_option + { optdepr = false; + optname = "behavior of non-imported hints"; + optkey = ["Loose"; "Hint"; "Behavior"]; + optread = read_warn_hint; + optwrite = write_warn_hint; + }) let fresh_key = let id = Summary.ref ~name:"HINT-COUNTER" 0 in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0beafb7e31..b3ea13cf4f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -61,7 +61,7 @@ let clear_hyp_by_default = ref false let use_clear_hyp_by_default () = !clear_hyp_by_default -let _ = +let () = declare_bool_option { optdepr = false; optname = "default clearing of hypotheses after use"; @@ -77,7 +77,7 @@ let universal_lemma_under_conjunctions = ref false let accept_universal_lemma_under_conjunctions () = !universal_lemma_under_conjunctions -let _ = +let () = declare_bool_option { optdepr = false; optname = "trivial unification in tactics applying under conjunctions"; @@ -96,7 +96,7 @@ let bracketing_last_or_and_intro_pattern = ref true let use_bracketing_last_or_and_intro_pattern () = !bracketing_last_or_and_intro_pattern -let _ = +let () = declare_bool_option { optdepr = false; optname = "bracketing last or-and introduction pattern"; @@ -4548,7 +4548,7 @@ let induction_gen_l isrec with_evars elim names lc = match EConstr.kind sigma c with | Var id when not (mem_named_context_val id (Global.named_context_val ())) && not with_evars -> - let _ = newlc:= id::!newlc in + let () = newlc:= id::!newlc in atomize_list l' | _ -> @@ -4561,7 +4561,7 @@ let induction_gen_l isrec with_evars elim names lc = let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in - let _ = newlc:=id::!newlc in + let () = newlc:=id::!newlc in Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v new file mode 100644 index 0000000000..10f955b41f --- /dev/null +++ b/test-suite/bugs/closed/bug_8364.v @@ -0,0 +1,17 @@ +Unset Primitive Projections. + +Record Box (A:Type) := box { unbox : A }. +Arguments box {_} _. Arguments unbox {_} _. + +Definition map {A B} (f:A -> B) x := + match x with box x => box (f x) end. + +Definition tuple (l : Box Type) : Type := + match l with + | box x => x + end. + +Fail Inductive stack : Type -> Type := +| Stack T foos : + tuple (map stack foos) -> + stack T. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index fb6d07d6cf..b248b87880 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -119,7 +119,8 @@ let compile opts ~echo ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in + let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in + let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -148,6 +149,8 @@ let compile opts ~echo ~f_in ~f_out = document anyways. *) let stm_options = let open Stm.AsyncOpts in { stm_options with + async_proofs_mode = APon; + async_proofs_n_workers = 0; async_proofs_cmd_error_resilience = false; async_proofs_tac_error_resilience = `None; } in diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 2f84eb9851..b98535b201 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -543,10 +543,6 @@ let parse_args arglist : coq_cmdopts * string list = (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - { oval with stm_flags = { oval.stm_flags with - Stm.AsyncOpts.async_proofs_full = true; - }} |"-async-proofs-never-reopen-branch" -> { oval with stm_flags = { oval.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true diff --git a/vernac/attributes.ml b/vernac/attributes.ml index bc0b0310b3..75ca027332 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -162,7 +162,7 @@ let universe_transform ~warn_unqualified : unit attribute = let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] let is_universe_polymorphism = let b = ref false in - let _ = let open Goptions in + let () = let open Goptions in declare_bool_option { optdepr = false; optname = "universe polymorphism"; diff --git a/vernac/classes.ml b/vernac/classes.ml index 95e46b252b..7d6bd1ca64 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -30,13 +30,13 @@ open Entries let refine_instance = ref true -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "definition of instances by refining"; - Goptions.optkey = ["Refine";"Instance";"Mode"]; - Goptions.optread = (fun () -> !refine_instance); - Goptions.optwrite = (fun b -> refine_instance := b) -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "definition of instances by refining"; + optkey = ["Refine";"Instance";"Mode"]; + optread = (fun () -> !refine_instance); + optwrite = (fun b -> refine_instance := b) +}) let typeclasses_db = "typeclass_instances" @@ -44,7 +44,7 @@ let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) -let _ = +let () = Hook.set Typeclasses.add_instance_hint_hook (fun inst path local info poly -> let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 4cdc60216e..4b8371f5c3 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -26,7 +26,7 @@ open Entries let axiom_into_instance = ref false -let _ = +let () = let open Goptions in declare_bool_option { optdepr = true; diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8507ee6e2c..8b9cf7d269 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -37,7 +37,7 @@ module RelDecl = Context.Rel.Declaration let should_auto_template = let open Goptions in let auto = ref true in - let _ = declare_bool_option + let () = declare_bool_option { optdepr = false; optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c1343fb592..9bd095aa52 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -44,7 +44,7 @@ open Context.Rel.Declaration (* Flags governing automatic synthesis of schemes *) let elim_flag = ref true -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of induction schemes"; @@ -53,7 +53,7 @@ let _ = optwrite = (fun b -> elim_flag := b) } let bifinite_elim_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of induction schemes for non-recursive types"; @@ -62,7 +62,7 @@ let _ = optwrite = (fun b -> bifinite_elim_flag := b) } let case_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of case analysis schemes"; @@ -71,7 +71,7 @@ let _ = optwrite = (fun b -> case_flag := b) } let eq_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of boolean equality"; @@ -82,7 +82,7 @@ let _ = let is_eq_flag () = !eq_flag let eq_dec_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of decidable equality"; @@ -91,7 +91,7 @@ let _ = optwrite = (fun b -> eq_dec_flag := b) } let rewriting_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname ="automatic declaration of rewriting schemes for equality types"; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 46d7892bf6..28e80a74aa 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -450,7 +450,7 @@ let start_proof_com ?inference_hook kind thms hook = let keep_admitted_vars = ref true -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 8baf391c70..cbb77057bd 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -343,7 +343,7 @@ let set_hide_obligations = (:=) hide_obligations let get_hide_obligations () = !hide_obligations open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Hiding of Program obligations"; @@ -356,7 +356,7 @@ let shrink_obligations = ref true let set_shrink_obligations = (:=) shrink_obligations let get_shrink_obligations () = !shrink_obligations -let _ = +let () = declare_bool_option { optdepr = true; (* remove in 8.8 *) optname = "Shrinking of Program obligations"; @@ -893,7 +893,7 @@ let obligation_terminator name num guard hook auto pf = let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in - let _ = obls.(num) <- obl in + let () = obls.(num) <- obl in let prg_ctx = if pi2 (prg.prg_kind) then (* Polymorphic *) (** We merge the new universes and constraints of the @@ -949,7 +949,7 @@ in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in let () = if transparent then add_hint true prg cst in let obls = Array.copy obls in - let _ = obls.(num) <- obl in + let () = obls.(num) <- obl in let prg = { prg with prg_ctx = ctx' } in let () = try ignore (update_obls prg obls (pred rem)) @@ -1045,7 +1045,7 @@ and solve_prg_obligations prg ?oblset tac = (fun i -> Int.Set.mem i !set) in let prgref = ref prg in - let _ = + let () = Array.iteri (fun i x -> if p i then match solve_obligation_by_tac !prgref obls' i tac with @@ -1132,7 +1132,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in + let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 3e2bd98720..526845084a 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -137,13 +137,13 @@ let suggest_common env ppid used ids_typ skip = let suggest_proof_using = ref false -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "suggest Proof using"; - Goptions.optkey = ["Suggest";"Proof";"Using"]; - Goptions.optread = (fun () -> !suggest_proof_using); - Goptions.optwrite = ((:=) suggest_proof_using) } +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "suggest Proof using"; + optkey = ["Suggest";"Proof";"Using"]; + optread = (fun () -> !suggest_proof_using); + optwrite = ((:=) suggest_proof_using) }) let suggest_constant env kn = if !suggest_proof_using @@ -172,13 +172,13 @@ let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) -let _ = - Goptions.declare_stringopt_option - { Goptions.optdepr = false; - Goptions.optname = "default value for Proof using"; - Goptions.optkey = ["Default";"Proof";"Using"]; - Goptions.optread = (fun () -> Option.map using_to_string !value); - Goptions.optwrite = (fun b -> value := Option.map using_from_string b); - } +let () = + Goptions.(declare_stringopt_option + { optdepr = false; + optname = "default value for Proof using"; + optkey = ["Default";"Proof";"Using"]; + optread = (fun () -> Option.map using_to_string !value); + optwrite = (fun b -> value := Option.map using_from_string b); + }) let get_default_proof_using () = !value diff --git a/vernac/record.ml b/vernac/record.ml index 7bdf6a973f..81b33c2e11 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -36,7 +36,7 @@ module RelDecl = Context.Rel.Declaration (** Flag governing use of primitive projections. Disabled by default. *) let primitive_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "use of primitive projections"; @@ -45,7 +45,7 @@ let _ = optwrite = (fun b -> primitive_flag := b) } let typeclasses_strict = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "strict typeclass resolution"; @@ -54,7 +54,7 @@ let _ = optwrite = (fun b -> typeclasses_strict := b); } let typeclasses_unique = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "unique typeclass instances"; @@ -103,7 +103,7 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields finite def poly pl ps records = let env0 = Global.env () in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in - let _ = + let () = let error bk {CAst.loc; v=name} = match bk, name with | Default _, Anonymous -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a78329ad1d..fa1082473e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1409,7 +1409,7 @@ let vernac_generalizable ~local = let local = Option.default true local in Implicit_quantifiers.declare_generalizable ~local -let _ = +let () = declare_bool_option { optdepr = false; optname = "silent"; @@ -1417,7 +1417,7 @@ let _ = optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit arguments"; @@ -1425,7 +1425,7 @@ let _ = optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "strict implicit arguments"; @@ -1433,7 +1433,7 @@ let _ = optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "strong strict implicit arguments"; @@ -1441,7 +1441,7 @@ let _ = optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "contextual implicit arguments"; @@ -1449,7 +1449,7 @@ let _ = optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit status of reversible patterns"; @@ -1457,7 +1457,7 @@ let _ = optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "maximal insertion of implicit"; @@ -1465,7 +1465,7 @@ let _ = optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "coercion printing"; @@ -1473,7 +1473,7 @@ let _ = optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "printing of existential variable instances"; @@ -1481,7 +1481,7 @@ let _ = optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit arguments printing"; @@ -1489,7 +1489,7 @@ let _ = optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit arguments defensive printing"; @@ -1497,7 +1497,7 @@ let _ = optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "projection printing using dot notation"; @@ -1505,7 +1505,7 @@ let _ = optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "notations printing"; @@ -1513,7 +1513,7 @@ let _ = optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "raw printing"; @@ -1521,7 +1521,7 @@ let _ = optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "use of the program extension"; @@ -1529,7 +1529,7 @@ let _ = optread = (fun () -> !Flags.program_mode); optwrite = (fun b -> Flags.program_mode:=b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Polymorphic inductive cumulativity"; @@ -1537,7 +1537,7 @@ let _ = optread = Flags.is_polymorphic_inductive_cumulativity; optwrite = Flags.make_polymorphic_inductive_cumulativity } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Uniform inductive parameters"; @@ -1545,7 +1545,7 @@ let _ = optread = (fun () -> !uniform_inductive_parameters); optwrite = (fun b -> uniform_inductive_parameters := b) } -let _ = +let () = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; @@ -1555,7 +1555,7 @@ let _ = let lev = Option.default Flags.default_inline_level o in Flags.set_inline_level lev) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "kernel term sharing"; @@ -1563,7 +1563,7 @@ let _ = optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); optwrite = Global.set_share_reduction } -let _ = +let () = declare_bool_option { optdepr = false; optname = "display compact goal contexts"; @@ -1571,7 +1571,7 @@ let _ = optread = (fun () -> Printer.get_compact_context()); optwrite = (fun b -> Printer.set_compact_context b) } -let _ = +let () = declare_int_option { optdepr = false; optname = "the printing depth"; @@ -1579,7 +1579,7 @@ let _ = optread = Topfmt.get_depth_boxes; optwrite = Topfmt.set_depth_boxes } -let _ = +let () = declare_int_option { optdepr = false; optname = "the printing width"; @@ -1587,7 +1587,7 @@ let _ = optread = Topfmt.get_margin; optwrite = Topfmt.set_margin } -let _ = +let () = declare_bool_option { optdepr = false; optname = "printing of universes"; @@ -1595,7 +1595,7 @@ let _ = optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "dumping bytecode after compilation"; @@ -1603,7 +1603,7 @@ let _ = optread = (fun () -> !Cbytegen.dump_bytecode); optwrite = (:=) Cbytegen.dump_bytecode } -let _ = +let () = declare_bool_option { optdepr = false; optname = "dumping VM lambda code after compilation"; @@ -1611,7 +1611,7 @@ let _ = optread = (fun () -> !Clambda.dump_lambda); optwrite = (:=) Clambda.dump_lambda } -let _ = +let () = declare_bool_option { optdepr = false; optname = "explicitly parsing implicit arguments"; @@ -1619,7 +1619,7 @@ let _ = optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } -let _ = +let () = declare_string_option ~preprocess:CWarnings.normalize_flags_string { optdepr = false; optname = "warnings display"; @@ -1627,7 +1627,7 @@ let _ = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } -let _ = +let () = declare_string_option { optdepr = false; optname = "native_compute profiler output"; @@ -1635,7 +1635,7 @@ let _ = optread = Nativenorm.get_profile_filename; optwrite = Nativenorm.set_profile_filename } -let _ = +let () = declare_bool_option { optdepr = false; optname = "enable native compute profiling"; @@ -1933,7 +1933,7 @@ let interp_search_about_item env sigma = *) let search_output_name_only = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "output-name-only search"; @@ -2303,13 +2303,13 @@ let interp ?proof ~atts ~st c = let default_timeout = ref None -let _ = - Goptions.declare_int_option - { Goptions.optdepr = false; - Goptions.optname = "the default timeout"; - Goptions.optkey = ["Default";"Timeout"]; - Goptions.optread = (fun () -> !default_timeout); - Goptions.optwrite = ((:=) default_timeout) } +let () = + declare_int_option + { optdepr = false; + optname = "the default timeout"; + optkey = ["Default";"Timeout"]; + optread = (fun () -> !default_timeout); + optwrite = ((:=) default_timeout) } (** When interpreting a command, the current timeout is initially the default one, but may be modified locally by a Timeout command. *) |