diff options
| author | Arnaud Spiwack | 2014-09-03 18:16:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:55 +0200 |
| commit | a93104d5462894d5d0651aa2e04e12c311eb5897 (patch) | |
| tree | 8619451aa37d699fc012f0e5f6509560d9c46726 /parsing | |
| parent | 06e6a7b5a0d15f493a3f94fad905af2c44be9c09 (diff) | |
Remove [Infer] option of records.
Dead code formerly used by the now defunct [autoinstances].
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3437256ed2..f7f049884b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -200,7 +200,7 @@ GEXTEND Gram indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (priv,f,false,indl) + VernacInductive (priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -222,13 +222,13 @@ GEXTEND Gram gallina_ext: [ [ priv = private_token; - b = record_token; infer = infer_token; oc = opt_coercion; name = identref; + b = record_token; oc = opt_coercion; name = identref; ps = binders; s = OPT [ ":"; s = lconstr -> s ]; cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> let (recf,indf) = b in - VernacInductive (priv,indf,infer,[((oc,name),ps,s,recf,cfs),[]]) + VernacInductive (priv,indf,[((oc,name),ps,s,recf,cfs),[]]) ] ] ; thm_token: @@ -272,9 +272,6 @@ GEXTEND Gram | "CoInductive" -> (CoInductive,CoFinite) | "Variant" -> (Variant,BiFinite) ] ] ; - infer_token: - [ [ IDENT "Infer" -> true | -> false ] ] - ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; |