K.conclude_method = method_name;
K.conclude_args =
K.Aux (string_of_int no_constructors)
- ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
+ ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
::method_args@other_method_args;
K.conclude_conclusion =
try Some
conclude.Con.conclude_method = "Exists" ||
conclude.Con.conclude_method = "FalseInd") then
(match (List.tl conclude.Con.conclude_args) with
- Con.Term (C.AAppl
- id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
+ Con.Term (C.AAppl (
+ id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
let cargs = args2cic premise_env args in
let l' =
List.map
(function
- None -> P.Mo [] "_"
+ None -> P.Mo([],"_")
| Some t -> cexpr2pres t
) l
in
let l' =
List.map
(function
- None -> P.Mo [] "_"
+ None -> P.Mo([],"_")
| Some t -> cexpr2pres t
) l
in
(* *)
(***************************************************************************)
+let p_mtr a b = Mpresentation.Mtr(a,b)
+let p_mtd a b = Mpresentation.Mtd(a,b)
+let p_mtable a b = Mpresentation.Mtable(a,b)
+let p_mtext a b = Mpresentation.Mtext(a,b)
+let p_mi a b = Mpresentation.Mi(a,b)
+let p_mo a b = Mpresentation.Mo(a,b)
+let p_mrow a b = Mpresentation.Mrow(a,b)
+let p_mphantom a b = Mpresentation.Mphantom(a,b)
+
+
let rec split n l =
if n = 0 then [],l
else let l1,l2 =
| _ -> assert false) in
(match conclude.Con.conclude_conclusion with
None ->
- P.Mrow []
- [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+ p_mrow []
+ [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
| Some c -> let conclusion = term2pres c in
make_row
[arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
let module P = Mpresentation in
match obj with
`Def (K.Const,thesis,`Proof p) ->
- P.Mtable
+ p_mtable
[None,"align","baseline 1";
None,"equalrows","false";
None,"columnalign","left";
None,"helm:xref","id"]
- ([P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext []
+ ([p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext []
("UNFINISHED PROOF" ^ id ^"(" ^
String.concat " ; " (List.map UriManager.string_of_uri params)^
")")])] ;
- P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext [] "THESIS:"])] ;
- P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mphantom []
- (P.Mtext [] "__") ;
+ p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext [] "THESIS:"])] ;
+ p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mphantom []
+ (p_mtext [] "__") ;
term2pres thesis])]] @
(match metasenv with
None -> []
| Some metasenv' ->
- [P.Mtr []
- [P.Mtd []
+ [p_mtr []
+ [p_mtd []
(* Conjectures are in their own table to make *)
(* diffing the DOM trees easier. *)
- (P.Mtable
+ (p_mtable
[None,"align","baseline 1";
None,"equalrows","false";
None,"columnalign","left"]
- ((P.Mtr []
- [P.Mtd []
- (P.Mrow []
- [P.Mtext [] "CONJECTURES:"])])::
+ ((p_mtr []
+ [p_mtd []
+ (p_mrow []
+ [p_mtext [] "CONJECTURES:"])])::
List.map
(function
(id,n,context,ty) ->
- P.Mtr []
- [P.Mtd []
- (P.Mrow [Some "helm", "xref", id]
+ p_mtr []
+ [p_mtd []
+ (p_mrow [Some "helm", "xref", id]
(List.map
(function
None ->
- P.Mrow []
- [ P.Mi [] "_" ;
- P.Mo [] ":?" ;
- P.Mi [] "_"]
+ p_mrow []
+ [ p_mi [] "_" ;
+ p_mo [] ":?" ;
+ p_mi [] "_"]
| Some (`Declaration d)
| Some (`Hypothesis d) ->
let
{ K.dec_name = dec_name ;
K.dec_type = ty } = d
in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match dec_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":" ;
+ p_mo [] ":" ;
term2pres ty]
| Some (`Definition d) ->
let
{ K.def_name = def_name ;
K.def_term = bo } = d
in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match def_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":=" ;
+ p_mo [] ":=" ;
term2pres bo]
| Some (`Proof p) ->
let proof_name = p.K.proof_name in
- P.Mrow []
- [ P.Mi []
+ p_mrow []
+ [ p_mi []
(match proof_name with
None -> "_"
| Some n -> n) ;
- P.Mo [] ":=" ;
+ p_mo [] ":=" ;
proof2pres term2pres p]
) (List.rev context) @
- [ P.Mo [] "|-" ] @
- [ P.Mi [] (string_of_int n) ;
- P.Mo [] ":" ;
+ [ p_mo [] "|-" ] @
+ [ p_mi [] (string_of_int n) ;
+ p_mo [] ":" ;
term2pres ty ]
))
]
) metasenv'
))]]
) @
- [P.Mtr []
- [P.Mtd []
- (P.Mrow []
+ [p_mtr []
+ [p_mtd []
+ (p_mrow []
[proof2pres term2pres p])]])
| _ -> raise ToDo
;;
let locate s =
let query =
- M.Property true M.RefineExact ["objectName"] [] [] [] []
- false (M.Const s)
+ M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) )
in M.StatQuery query
let unreferred target_pattern source_pattern =
let query =
- M.Bin M.BinFDiff
+ M.Bin (M.BinFDiff,
(
- M.Property false M.RefineExact [] [] [] [] []
- true (M.Const target_pattern)
- ) (
- M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
- true (M.Const source_pattern)
+ M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const target_pattern))
+ ), (
+ M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern))
- )
+ ))
in M.StatQuery query
let compose cl =
con "h:depth" (List.map U.string_of_depth d)
in
let property_must n c =
- M.Property true M.RefineExact [n] []
- (cons false c) [] [] false (M.Const "")
+ M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const ""))
in
let property_only n cl =
let cll = List.map (cons true) cl in
- M.Property false M.RefineExact [n] []
- ! univ cll [] false (M.Proj None (M.AVar "obj"))
+ M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj"))))
in
let rec aux = function
| [] -> ()
only := true;
let l = List.map U.string_of_position l in
univ := [(false, ["h:position"], set_val l)]; aux tail
- | T.MustObj r p d :: tail ->
+ | T.MustObj(r,p,d) :: tail ->
must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
- | T.MustSort s p d :: tail ->
+ | T.MustSort(s,p,d) :: tail ->
must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
- | T.MustRel p d :: tail ->
+ | T.MustRel(p,d) :: tail ->
must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
- | T.OnlyObj r p d :: tail ->
+ | T.OnlyObj(r,p,d) :: tail ->
onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
- | T.OnlySort s p d :: tail ->
+ | T.OnlySort(s,p,d) :: tail ->
onlysort := ([], s, p, d) :: ! onlysort; aux tail
- | T.OnlyRel p d :: tail ->
+ | T.OnlyRel(p,d) :: tail ->
onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
in
let rec iter f g = function
aux cl;
let must_query =
if ! must = [] then
- M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*")
+ M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*"))
else
- iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must
+ iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must
in
- let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in
- let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in
- let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in
+ let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in
+ let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in
+ let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in
let select_query x =
match ! onlyobj, ! onlysort, ! onlyrel with
| [], [], [] -> x
- | _, [], [] -> M.Select "obj" x onlyobj_val
- | [], _, [] -> M.Select "obj" x onlysort_val
- | [], [], _ -> M.Select "obj" x onlyrel_val
- | _, _, [] -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val)
- | _, [], _ -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val)
- | [], _, _ -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val)
- | _, _, _ -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val)
+ | _, [], [] -> M.Select("obj",x,onlyobj_val)
+ | [], _, [] -> M.Select("obj",x,onlysort_val)
+ | [], [], _ -> M.Select("obj",x,onlyrel_val)
+ | _, _, [] -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val)))
+ | _, [], _ -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val)))
+ | [], _, _ -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val)))
+ | _, _, _ -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val)))
in
let letin_query =
if ! letin = [] then fun x -> x
else
- let f (vvar, msval) x = M.LetVVar vvar msval x in
+ let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in
iter f (fun x y z -> x (y z)) ! letin
in
M.StatQuery (letin_query (select_query must_query))
| M.True -> U.mql_true
| M.Const s -> [s]
| M.Set l -> U.iter (eval_val c) l
- | M.Test k y1 y2 ->
+ | M.Test (k,y1,y2) ->
let cand y1 y2 =
if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2
in
| M.VVar i -> begin
try List.assoc i c.vvars
with Not_found -> warn (M.Subj (M.VVar i)); [] end
- | M.Dot i p -> begin
+ | M.Dot (i,p) -> begin
try List.assoc p (List.assoc i c.groups)
- with Not_found -> warn (M.Subj (M.Dot i p)); [] end
- | M.Proj None x -> List.map (fun (r, _) -> r) (eval_query c x)
- | M.Proj (Some p) x ->
+ with Not_found -> warn (M.Subj (M.Dot (i,p))); [] end
+ | M.Proj (None,x) -> List.map (fun (r, _) -> r) (eval_query c x)
+ | M.Proj ((Some p),x) ->
let proj_group_aux (q, v) = if q = p then v else [] in
let proj_group a = U.iter proj_group_aux a in
let proj_set (_, g) = U.iter proj_group g in
U.iter proj_set (eval_query c x)
- | M.Ex l y ->
+ | M.Ex (l,y) ->
let rec ex_aux h = function
| [] ->
let d = {c with groups = h} in
C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
r
| M.Count y -> [string_of_int (List.length (eval_val c y))]
- | M.Align s y -> U.iter (U.align s) (eval_val c y)
+ | M.Align (s,y) -> U.iter (U.align s) (eval_val c y)
and eval_query c = function
| M.Empty -> []
| M.Subj x ->
List.map (fun s -> (s, [])) (eval_val c x)
- | M.Log _ b x ->
+ | M.Log (_,b,x) ->
if b then begin
let t = P.start_time () in
P.text_of_query (C.log h) x "\n";
C.log h (Printf.sprintf "Log: %s\n" r);
s
end
- | M.If y x1 x2 ->
+ | M.If (y,x1,x2) ->
if (eval_val c y) = U.mql_false
then (eval_query c x2) else (eval_query c x1)
- | M.Bin k x1 x2 ->
+ | M.Bin (k,x1,x2) ->
let f = match k with
| M.BinFJoin -> U.mql_union
| M.BinFMeet -> U.mql_intersect
| M.AVar i -> begin
try [List.assoc i c.avars]
with Not_found -> warn (M.AVar i); [] end
- | M.LetSVar i x1 x2 ->
+ | M.LetSVar (i,x1,x2) ->
let d = {c with svars = U.set (i, eval_query c x1) c.svars} in
eval_query d x2
- | M.LetVVar i y x ->
+ | M.LetVVar (i,y,x) ->
let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in
eval_query d x
- | M.For k i x1 x2 ->
+ | M.For (k,i,x1,x2) ->
let f = match k with
| M.GenFJoin -> U.mql_union
| M.GenFMeet -> U.mql_intersect
f (eval_query d x2) (for_aux t)
in
for_aux (eval_query c x1)
- | M.Add b z x ->
+ | M.Add (b,z,x) ->
let f = if b then U.mql_prod else U.set_union in
let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in
List.fold_right g (eval_query c x) []
- | M.Property q0 q1 q2 mc ct cfl el pat y ->
+ | M.Property (q0,q1,q2,mc,ct,cfl,el,pat,y) ->
let subj, mct =
if q0 then [], (pat, q2 @ mc, eval_val c y)
else (q2 @ mc), (pat, [], eval_val c y)
let s = P.stop_time t in
C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
r
- | M.Select i x y ->
+ | M.Select (i,x,y) ->
let rec select_aux = function
| [] -> []
| h :: t ->
then select_aux t else h :: select_aux t
in
select_aux (eval_query c x)
- | M.Keep b l x ->
+ | M.Keep (b,l,x) ->
let keep_path (p, v) t =
if List.mem p l = b then t else (p, v) :: t in
let keep_grp a = List.fold_right keep_path a [] in
| M.Const _ -> []
| M.VVar _ -> []
| M.Ex _ -> []
- | M.Dot rv _ -> [rv]
+ | M.Dot (rv,_) -> [rv]
| M.Not x -> an_val x
| M.StatVal x -> an_val x
| M.Count x -> an_val x
- | M.Align _ x -> an_val x
- | M.Proj _ x -> an_set x
- | M.Test _ x y -> iter an_val [x; y]
+ | M.Align (_,x) -> an_val x
+ | M.Proj (_,x) -> an_set x
+ | M.Test (_,x,y) -> iter an_val [x; y]
| M.Set l -> iter an_val l
and an_set = function
| M.Empty -> []
| M.SVar _ -> []
| M.AVar _ -> []
| M.Subj x -> an_val x
- | M.Keep _ _ x -> an_set x
- | M.Log _ _ x -> an_set x
+ | M.Keep (_,_,x) -> an_set x
+ | M.Log (_,_,x) -> an_set x
| M.StatQuery x -> an_set x
- | M.Bin _ x y -> iter an_set [x; y]
- | M.LetSVar _ x y -> iter an_set [x; y]
- | M.For _ _ x y -> iter an_set [x; y]
- | M.Add _ g x -> join (an_grp g) (an_set x)
- | M.LetVVar _ x y -> join (an_val x) (an_set y)
- | M.Select _ x y -> join (an_set x) (an_val y)
- | M.Property _ _ _ _ c d _ _ x ->
+ | M.Bin (_,x,y) -> iter an_set [x; y]
+ | M.LetSVar (_,x,y) -> iter an_set [x; y]
+ | M.For (_,_,x,y) -> iter an_set [x; y]
+ | M.Add (_,g,x) -> join (an_grp g) (an_set x)
+ | M.LetVVar (_,x,y) -> join (an_val x) (an_set y)
+ | M.Select (_,x,y) -> join (an_set x) (an_val y)
+ | M.Property (_,_,_,_,c,d,_,_,x) ->
join (an_val x) (iter an_con [c; List.concat d])
- | M.If x y z -> join (an_val x) (iter an_set [y; z])
+ | M.If (x,y,z) -> join (an_val x) (iter an_set [y; z])
and fc (_, _, v) = an_val v
and an_con c = iter fc c
and fg (_, v) = an_val v
| TRUE { M.True }
| FALSE { M.False }
| STR { M.Const $1 }
- | avar FS path { M.Dot $1 $3 }
+ | avar FS path { M.Dot ($1,$3) }
| vvar { M.VVar $1 }
| LC vals RC { M.Set $2 }
| LC RC { M.Set [] }
| LP val_exp RP { $2 }
| STAT val_exp { M.StatVal $2 }
- | EX val_exp { M.Ex (analyze $2) $2 }
+ | EX val_exp { M.Ex ((analyze $2),$2) }
| NOT val_exp { M.Not $2 }
- | test_op { M.Test (f $1) (s $1) (t $1) }
- | PROJ opt_path set_exp { M.Proj $2 $3 }
+ | test_op { M.Test ((f $1),(s $1),(t $1)) }
+ | PROJ opt_path set_exp { M.Proj ($2,$3) }
| COUNT val_exp { M.Count $2 }
- | ALIGN STR IN val_exp { M.Align $2 $4 }
+ | ALIGN STR IN val_exp { M.Align ($2,$4) }
;
vals:
| val_exp CM vals { $1 :: $3 }
| LP set_exp RP { $2 }
| svar { M.SVar $1 }
| avar { M.AVar $1 }
- | LET svar BE set_exp IN set_exp { M.LetSVar $2 $4 $6 }
- | LET vvar BE val_exp IN set_exp { M.LetVVar $2 $4 $6 }
+ | LET svar BE set_exp IN set_exp { M.LetSVar ($2,$4,$6) }
+ | LET vvar BE val_exp IN set_exp { M.LetVVar ($2,$4,$6) }
| FOR avar IN set_exp gen_op
- { M.For (fst $5) $2 $4 (snd $5) }
- | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 }
- | IF val_exp THEN set_exp ELSE set_exp { M.If $2 $4 $6 }
+ { M.For ((fst $5),$2,$4,(snd $5)) }
+ | ADD distr grp_exp IN set_exp { M.Add ($2,$3,$5) }
+ | IF val_exp THEN set_exp ELSE set_exp { M.If ($2,$4,$6) }
| PROP qualif mainc istrue isfalse attrc OF pattern val_exp
- { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 }
- | LOG xml source set_exp { M.Log $2 $3 $4 }
+ { M.Property ((f $2),(s $2),(t $2),$3,$4,$5,$6,$8,$9) }
+ | LOG xml source set_exp { M.Log ($2,$3,$4) }
| STAT set_exp { M.StatQuery $2 }
- | KEEP allbut paths IN set_exp { M.Keep $2 $3 $5 }
- | KEEP allbut IN set_exp { M.Keep $2 [] $4 }
+ | KEEP allbut paths IN set_exp { M.Keep ($2,$3,$5) }
+ | KEEP allbut IN set_exp { M.Keep ($2,[],$4) }
| bin_op
- { M.Bin (f $1) (s $1) (t $1) }
- | SELECT avar FROM set_exp WHERE val_exp { M.Select $2 $4 $6 }
+ { M.Bin ((f $1),(s $1),(t $1)) }
+ | SELECT avar FROM set_exp WHERE val_exp { M.Select ($2,$4,$6) }
| SUBJ val_exp { M.Subj $2 }
;
query:
| M.Const s -> txt_str out s
| M.Set l -> txt_val_list l
| M.VVar vv -> txt_vvar vv
- | M.Dot av p -> txt_avar av; out "."; txt_path out p
- | M.Proj op x -> out "proj "; txt_opt_path op; txt_set x
- | M.Ex b x -> out "ex "; txt_val x
+ | M.Dot (av,p) -> txt_avar av; out "."; txt_path out p
+ | M.Proj (op,x) -> out "proj "; txt_opt_path op; txt_set x
+ | M.Ex (b,x) -> out "ex "; txt_val x
(* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x
*) | M.Not x -> out "not "; txt_val x
- | M.Test k x y -> out "("; txt_val x; txt_test k; txt_val y; out ")"
+ | M.Test (k,x,y) -> out "("; txt_val x; txt_test k; txt_val y; out ")"
| M.StatVal x -> out "stat "; txt_val x
| M.Count x -> out "count "; txt_val x
- | M.Align s x -> out "align "; txt_str out s; out " in "; txt_val x
+ | M.Align (s,x) -> out "align "; txt_str out s; out " in "; txt_val x
and txt_set = function
| M.Empty -> out "empty"
| M.SVar sv -> txt_svar sv
| M.AVar av -> txt_avar av
- | M.Property q0 q1 q2 mc ct cfl xl b x ->
+ | M.Property (q0,q1,q2,mc,ct,cfl,xl,b,x) ->
out "property "; txt_qualif q0 q1 q2; main mc;
txt_istrue ct; txt_list out txt_isfalse "" cfl; txt_exp_list xl;
out " of "; pattern b; txt_val x
- | M.Bin k x y -> out "("; txt_set x; txt_bin k; txt_set y;
+ | M.Bin (k,x,y) -> out "("; txt_set x; txt_bin k; txt_set y;
out ")"
- | M.LetSVar sv x y -> out "let "; txt_svar sv; out " be ";
+ | M.LetSVar (sv,x,y) -> out "let "; txt_svar sv; out " be ";
txt_set x; out " in "; txt_set y
- | M.LetVVar vv x y -> out "let "; txt_vvar vv; out " be ";
+ | M.LetVVar (vv,x,y) -> out "let "; txt_vvar vv; out " be ";
txt_val x; out " in "; txt_set y
- | M.Select av x y -> out "select "; txt_avar av; out " from ";
+ | M.Select (av,x,y) -> out "select "; txt_avar av; out " from ";
txt_set x; out " where "; txt_val y
| M.Subj x -> out "subj "; txt_val x
- | M.For k av x y -> out "for "; txt_avar av; out " in ";
+ | M.For (k,av,x,y) -> out "for "; txt_avar av; out " in ";
txt_set x; txt_gen k; txt_set y
- | M.If x y z -> out "if "; txt_val x; out " then ";
+ | M.If (x,y,z) -> out "if "; txt_val x; out " then ";
txt_set y; out " else "; txt_set z
- | M.Add d g x -> out "add "; txt_distr d; txt_grp g;
+ | M.Add (d,g,x) -> out "add "; txt_distr d; txt_grp g;
out " in "; txt_set x
- | M.Log a b x -> out "log "; txt_log a b; txt_set x
+ | M.Log (a,b,x) -> out "log "; txt_log a b; txt_set x
| M.StatQuery x -> out "stat "; txt_set x
- | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l;
+ | M.Keep (b,l,x) -> out "keep "; txt_allbut b; txt_path_list l;
txt_set x
in
txt_set x; out sep
C.Lambda (binder,source,(aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
- else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
+ then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
+ else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
EliminationTactics.elim_type_tac
- ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )
+ ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
~status
in
(match goals' with
projects / helm.git / commitdiff