]> matita.cs.unibo.it Git - helm.git/commitdiff
Patch to make it compile with recent OCaml
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Dec 2017 18:13:02 +0000 (19:13 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Dec 2017 18:13:02 +0000 (19:13 +0100)
helm/software/components/content_pres/content2pres.ml

index 05e4ae3cbd8d55532a9cb51ba41b3324989f8389..d9255f220d02247026943886f1515e96d1194a27 100644 (file)
@@ -1013,7 +1013,8 @@ let njoint_def2pres term2pres joint_kind defs =
 ;;
 
 let content2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj) 
 =
   match obj with
@@ -1070,7 +1071,8 @@ let content2pres
           (TermContentPres.pp_ast ast)))
 
 let ncontent2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
 =
   match obj with