| NBlock of loc * ntactic list
(* Declarative langauge *)
(* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
- | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
- | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
- | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc,
- justification, conclusion, identifier, eqconcl *)
- | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
- identifier, equivnewcon *)
+ | Assume of loc * string * nterm (* loc, identifier, type *)
+ | Suppose of loc * nterm * string (* loc, assumption, identifier *)
+ | By_just_we_proved of loc * just * nterm * string option (* loc, justification, conclusion, identifier *)
+ | We_need_to_prove of loc * nterm * string option (* loc, newconclusion, identifier *)
| BetaRewritingStep of loc * nterm
| Bydone of loc * just
| ExistsElim of loc * just * string * nterm * nterm * string
| AndElim of loc * just * nterm * string * nterm * string
- (*
- | RewritingStep of
- loc * (string option * nterm) option * nterm *
- [ `Term of nterm | `Auto of auto_params
- | `Proof | `SolveWith of nterm ] *
- bool (* last step*)
- *)
| RewritingStep of
loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*)
| Obtain of
loc * string * nterm
| Conclude of
loc * nterm
- | Thesisbecomes of loc * nterm * nterm option
+ | Thesisbecomes of loc * nterm
| We_proceed_by_induction_on of loc * nterm * nterm
| We_proceed_by_cases_on of loc * nterm * nterm
| Byinduction of loc * nterm * string
| NBlock (_,l) ->
"(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
| NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
- | Assume (_, ident, term, term1) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term ^
- (match term1 with None -> " " | Some t1 -> " that is eqivalent to " ^ NotationPp.pp_term status t1)
- | Suppose (_,term,ident,term1) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" ^ (match
- term1 with None -> " " | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t)
- | By_just_we_proved (_, just, term1, ident, term2) -> pp_just status just ^ "we proved" ^
- NotationPp.pp_term status term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match
- term2 with None -> " " | Some term2 -> " that is equivalent to " ^ NotationPp.pp_term status term2)
- | We_need_to_prove (_,term,ident,t) -> "we need to prove" ^ NotationPp.pp_term status term ^
- (match ident with None -> " " | Some id -> "(" ^ id ^ ")") ^ (match t with None -> "" | Some t ->
- " or equivalently " ^ (NotationPp.pp_term status t))
- | BetaRewritingStep (_,t) -> "or equivalently " ^ (NotationPp.pp_term status t)
+ | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term
+ | Suppose (_,term,ident) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")"
+ | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ "we proved" ^
+ NotationPp.pp_term status term1 ^ (match ident with
+ None -> "" | Some ident -> "(" ^ident^ ")")
+ | We_need_to_prove (_,term,ident) -> "we need to prove" ^ NotationPp.pp_term status term ^
+ (match ident with None -> "" | Some id -> "(" ^ id ^ ")")
+ | BetaRewritingStep (_,t) -> "that is equivalent to" ^ (NotationPp.pp_term status t)
| Bydone (_, just) -> pp_just status just ^ "done"
| ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":"
- ^ NotationPp.pp_term status term ^ "such that " ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
+ ^ NotationPp.pp_term status term ^ "such that" ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
| AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^
NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2
^ " (" ^ ident2 ^ ")"
- | Thesisbecomes (_, t, t1) -> "the thesis becomes " ^ NotationPp.pp_term status t ^
- (match t1 with None -> "" | Some t1 -> " or equivalently " ^
- NotationPp.pp_term status
- t1)
+ | Thesisbecomes (_, t) -> "the thesis becomes" ^ NotationPp.pp_term status t
| RewritingStep (_, rhs, just, cont) ->
"=" ^
NotationPp.pp_term status rhs ^
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
|GrafiteAst.NRepeat (_,tac) ->
NTactics.repeat_tac (f f (text, prefix_len, tac))
- |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None ->
- None | Some t1 -> (Some (text,prefix_len,t1)))
- |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None
- -> None | Some t1 -> (Some (text,prefix_len,t1)))
- |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
- (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
- Some t2 -> (Some (text,prefix_len,t2)))
- |GrafiteAst.We_need_to_prove (_, t, id, t1) -> Declarative.we_need_to_prove (text,prefix_len,t) id
- (match t1 with None -> None | Some t1 -> Some (text,prefix_len,t1))
+ |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t)
+ |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id
+ |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved
+ (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s
+ |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id
|GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t)
| GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
| GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
(text,prefix_len,t2) id2
| GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
- | GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1)
- (match t2 with None -> None | Some t2 -> Some (text,prefix_len,t2))
+ | GrafiteAst.Thesisbecomes (_, t1) -> Declarative.thesisbecomes (text,prefix_len,t1)
| GrafiteAst.RewritingStep (_,rhs,just,cont) ->
Declarative.rewritingstep (text,prefix_len,rhs)
(match just with
type by_continuation =
BYC_done
- | BYC_weproved of N.term * string option * N.term option
+ | BYC_weproved of N.term * string option
| BYC_letsuchthat of string * N.term * N.term * string
| BYC_wehaveand of string * N.term * string * N.term
| SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
| SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
| SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
- | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term ; t1 = OPT [IDENT "that"; IDENT "is";
- IDENT "equivalent"; "to"; t' = tactic_term -> t']-> G.NTactic (loc,[G.Assume (loc,id,t,t1)])
- | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT
- "is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)])
+ | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> G.NTactic (loc,[G.Suppose (loc,t,id)])
| "let"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
G.NTactic(loc,[G.NLetIn (loc,(None,[],Some N.UserInput),t,name)])
| just =
cont=by_continuation -> G.NTactic (loc,[
(match cont with
BYC_done -> G.Bydone (loc, just)
- | BYC_weproved (ty,id,t1) ->
- G.By_just_we_proved(loc, just, ty, id, t1)
+ | BYC_weproved (ty,id) ->
+ G.By_just_we_proved(loc, just, ty, id)
| BYC_letsuchthat (id1,t1,t2,id2) ->
G.ExistsElim (loc, just, id1, t1, t2, id2)
| BYC_wehaveand (id1,t1,id2,t2) ->
G.AndElim (loc, just, t1, id1, t2, id2))
])
- | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id =
-IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term ->
-t']->
- G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)])
- | IDENT "or"; IDENT "equivalently"; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])
- | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT
-"equivalently"; t2 = tactic_term -> t2] ->
- G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ->
+ G.NTactic (loc,[G.We_need_to_prove (loc, t, id)])
+ | IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])
+ | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term -> G.NTactic (loc,[G.Thesisbecomes(loc,t1)])
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])
| IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
];
by_continuation: [
- [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
- | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
- "done" -> BYC_weproved (ty,None,t1)
+ [ WEPROVED; ty = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id] -> BYC_weproved (ty,id)
| "done" -> BYC_done
| "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
status#set_stack ((g,t,k,tag,newp)::tl)
;;
+let add_parameter_tac key value status =
+ match status#stack with
+ [] -> status
+ | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
+;;
+
+
(* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
\lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
*)
-let lambda_abstract_tac id t1 t2 status goal =
+let lambda_abstract_tac id t1 status goal =
match extract_conclusion_type status goal with
| NCic.Prod (_,t,_) ->
if alpha_eq_tacterm_kerterm t1 t status goal then
+ let (_,_,t1) = t1 in
+ block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+ `JustOne))); clear_volatile_params_tac;
+ add_parameter_tac "volatile_newhypo" id] status
+(*
match t2 with
| None ->
let (_,_,t1) = t1 in
`JustOne))); clear_volatile_params_tac] status
else
raise NotEquivalentTypes
+*)
else
raise FirstTypeWrong
| _ -> raise NotAProduct
-let assume name ty eqty status =
+let assume name ty status =
let goal = extract_first_goal_from_status status in
- try lambda_abstract_tac name ty eqty status goal
+ try lambda_abstract_tac name ty status goal
with
| NotAProduct -> fail (lazy "You can't assume without an universal quantification")
| FirstTypeWrong -> fail (lazy "The assumed type is wrong")
| NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
;;
-let suppose t1 id t2 status =
+let suppose t1 id status =
let goal = extract_first_goal_from_status status in
- try lambda_abstract_tac id t1 t2 status goal
+ try lambda_abstract_tac id t1 status goal
with
| NotAProduct -> fail (lazy "You can't suppose without a logical implication")
| FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise")
let beta_rewriting_step t status =
let ctx = status_parameter "volatile_context" status in
- if ctx <> "beta_rewrite" then fail (lazy "Invalid use of 'or equivalently'")
+ if ctx <> "beta_rewrite" then
+ (
+ let newhypo = status_parameter "volatile_newhypo" status in
+ if newhypo = "" then
+ fail (lazy "Invalid use of 'or equivalently'")
+ else
+ change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status
+ )
else
change_tac ~where:("",0,(None,[],Some
Ast.UserInput)) ~with_what:t status
else status (* Nothing to push *)
| _ -> status
-let add_parameter_tac key value status =
- match status#stack with
- [] -> status
- | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
-;;
-
-let we_need_to_prove t id t1 status =
+let we_need_to_prove t id status =
let goal = extract_first_goal_from_status status in
match id with
| None ->
(
- match t1 with
- | None -> (* We need to prove t *)
- (
- try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
- with
- | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
- )
- | Some t1 -> (* We need to prove t or equivalently t1 *)
- (
- try assert_tac t (Some t1) status goal (block_tac [change_tac ~where:("",0,(None,[],Some
- Ast.UserInput))
- ~with_what:t1;
- add_parameter_tac "volatile_context"
- "beta_rewrite"] status)
- with
- | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
- | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
- )
+ try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
+ with
+ | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
)
| Some id ->
(
- match t1 with
- (* We need to prove t (id) *)
- | None -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
- push_goals_tac
+ block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+ push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite"
] status
- (* We need to prove t (id) or equivalently t1 *)
- | Some t1 -> block_tac [clear_volatile_params_tac; cut_tac t; branch_tac ; change_tac ~where:("",0,(None,[],Some
- Ast.UserInput))
- ~with_what:t1; shift_tac; intro_tac id; merge_tac;
- branch_tac; push_goals_tac
- ]
- status
)
;;
-let by_just_we_proved just ty id ty' status =
+let by_just_we_proved just ty id status =
let goal = extract_first_goal_from_status status in
let wrappedjust = just in
let just = mk_just status goal just in
match id with
| None ->
- (match ty' with
- | None -> (* just we proved P done *)
- (
- try
- assert_tac ty None status goal (bydone wrappedjust status)
- with
- | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
- | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
- )
- | Some ty' -> (* just we proved P that is equivalent to P' done *)
- (
- try
- assert_tac ty' None status goal (block_tac [change_tac ~where:("",0,(None,[],Some
- Ast.UserInput))
- ~with_what:ty; bydone wrappedjust]
- status )
- with
- | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
- | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
- )
- )
+ assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac
+ "volatile_context" "beta_rewrite"] status)
| Some id ->
(
- match ty' with
- | None -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
- clear_volatile_params_tac ] status
- | Some ty' -> block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; change_tac
- ~where:("",0,(None,[id,Ast.UserInput],None)) ~with_what:ty';
- merge_tac; clear_volatile_params_tac] status
+ block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+ clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status
)
;;
in
status#set_stack gstatus
-let thesisbecomes t1 l = we_need_to_prove t1 None l
+let thesisbecomes t1 = we_need_to_prove t1 None
;;
let obtain id t1 status =
| FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
;;
-let byinduction t1 id = suppose t1 id None ;;
+let byinduction t1 id = suppose t1 id ;;
let name_of_conj conj =
let mattrs,_,_ = conj in
match l with
[] -> [id_tac]
| (id,ty)::tl ->
- (try_tac (assume id ("",0,ty) None)) :: (aux tl)
+ (try_tac (assume id ("",0,ty))) :: (aux tl)
in
aux l
in
type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
-val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
-val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
-val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val assume : string -> NTacStatus.tactic_term -> 's NTacStatus.tactic
+val suppose : NTacStatus.tactic_term -> string -> 's NTacStatus.tactic
+val we_need_to_prove : NTacStatus.tactic_term -> string option -> 's NTacStatus.tactic
val beta_rewriting_step : NTacStatus.tactic_term -> 's NTacStatus.tactic
val bydone : just -> 's NTacStatus.tactic
-val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term
-option -> 's NTacStatus.tactic
+val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> 's NTacStatus.tactic
val andelim : just -> NTacStatus.tactic_term -> string -> NTacStatus.tactic_term -> string -> 's
NTacStatus.tactic
val existselim : just -> string -> NTacStatus.tactic_term -> NTacStatus.tactic_term -> string -> 's
NTacStatus.tactic
-val thesisbecomes : NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val thesisbecomes : NTacStatus.tactic_term -> 's NTacStatus.tactic
val rewritingstep : NTacStatus.tactic_term -> [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params
| `Proof | `SolveWith of NTacStatus.tactic_term ] ->
bool (* last step *) -> 's NTacStatus.tactic
let status, res = disambiguate status ctx t `XTNone in
let _,res = term_of_cic_term status res (ctx_of res)
in Ast.NCic res
- in Some (List.map to_Ast l)
+ in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
+ Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
+ Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
+ Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
+ ])
let auto_lowtac ~params:(univ,flags as params) status goal =
let gty = get_goalty status goal in
let ctx = ctx_of gty in
let candidates = candidates_from_ctx univ ctx status in
- auto_tac' candidates ~local_candidates:false ~use_given_only:true flags ~trace_ref:(ref [])
+ auto_tac' candidates ~local_candidates:false ~use_given_only:false flags ~trace_ref:(ref [])
let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let candidates = candidates_from_ctx univ [] status in
+utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi
+utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
utf8Macro.cmi :
utf8MacroTable.cmo :
utf8MacroTable.cmx :
-utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi
-utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
-applyTransformation.cmo : applyTransformation.cmi
applyTransformation.cmx : applyTransformation.cmi
-buildTimeConf.cmo :
+applyTransformation.cmi :
buildTimeConf.cmx :
-cicMathView.cmo : matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
- buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi
cicMathView.cmx : matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
-lablGraphviz.cmo : lablGraphviz.cmi
+cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi
lablGraphviz.cmx : lablGraphviz.cmi
-matitaclean.cmo : matitaMisc.cmi matitaInit.cmi matitaclean.cmi
-matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi
-matitac.cmo : matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
- matitaEngine.cmi
-matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
- matitaEngine.cmx
-matitaEngine.cmo : applyTransformation.cmi matitaEngine.cmi
+lablGraphviz.cmi :
+matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \
+ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \
+ applyTransformation.cmx
matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi
-matitaExcPp.cmo : matitaEngine.cmi matitaExcPp.cmi
+matitaEngine.cmi : applyTransformation.cmi
matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi
-matitaGeneratedGui.cmo :
+matitaExcPp.cmi :
matitaGeneratedGui.cmx :
-matitaGtkMisc.cmo : matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \
- matitaGtkMisc.cmi
matitaGtkMisc.cmx : matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
matitaGtkMisc.cmi
-matitaGui.cmo : matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
- matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi
+matitaGtkMisc.cmi : matitaGeneratedGui.cmx
matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo : matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi
+matitaGui.cmi : matitaGuiTypes.cmi
+matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi
matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
-matitaMathView.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \
- matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmx \
- applyTransformation.cmi matitaMathView.cmi
+matitaInit.cmi :
matitaMathView.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
applyTransformation.cmx matitaMathView.cmi
-matitaMisc.cmo : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
+matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi
matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
-matita.cmo : predefined_virtuals.cmi matitaScript.cmi matitaMisc.cmi \
- matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx \
- applyTransformation.cmi
-matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \
- matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \
- applyTransformation.cmx
-matitaScript.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
- buildTimeConf.cmx matitaScript.cmi
+matitaMisc.cmi : matitaGuiTypes.cmi
matitaScript.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \
buildTimeConf.cmx matitaScript.cmi
-matitaTypes.cmo : matitaTypes.cmi
-matitaTypes.cmx : matitaTypes.cmi
-predefined_virtuals.cmo : virtuals.cmi predefined_virtuals.cmi
-predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi
-virtuals.cmo : virtuals.cmi
-virtuals.cmx : virtuals.cmi
-applyTransformation.cmi :
-cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi
-lablGraphviz.cmi :
-matitaclean.cmi :
-matitaEngine.cmi : applyTransformation.cmi
-matitaExcPp.cmi :
-matitaGtkMisc.cmi : matitaGeneratedGui.cmx
-matitaGui.cmi : matitaGuiTypes.cmi
-matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi
-matitaInit.cmi :
-matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmi : matitaGuiTypes.cmi
matitaScript.cmi :
+matitaTypes.cmx : matitaTypes.cmi
matitaTypes.cmi :
+matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
+ matitaEngine.cmx
+matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi
+matitaclean.cmi :
+predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi
predefined_virtuals.cmi :
+virtuals.cmx : virtuals.cmi
virtuals.cmi :
projects / helm.git / commitdiff