diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-05 21:50:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-15 20:21:37 +0200 |
| commit | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (patch) | |
| tree | 76a95699918b818e3f6111b594b5b6ec7bd566b2 /stm | |
| parent | 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 (diff) | |
Remove the syntax changes introduced by this branch.
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 6 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4f014be2d..9edc1f1c7 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_,_, _, iednll) -> + | VernacInductive (_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin @@ -598,14 +598,14 @@ let rec tmpp v loc = (fun (ie, dnl) -> (pp_inductive_expr ie) @ (List.map pp_decl_notation dnl)) iednll) in xmlInductive kind loc exprs - | VernacFixpoint (_,_, fednll) -> + | VernacFixpoint (_, fednll) -> let exprs = List.flatten (* should probably not be flattened *) (List.map (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ (List.map pp_decl_notation dnl)) fednll) in xmlFixpoint exprs - | VernacCoFixpoint (_,_, cfednll) -> + | VernacCoFixpoint (_, cfednll) -> (* Nota: it is like VernacFixpoint without so could be merged *) let exprs = List.flatten (* should probably not be flattened *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 574cc0044..2b5eb8683 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -125,14 +125,14 @@ let rec classify_vernac e = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,_,l) -> + | VernacFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,_,l) -> + | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,_,l) -> + | VernacInductive (_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ |