-requires="helm-cic_proof_checking helm-acic_content helm-grafite"
+requires="helm-acic_content helm-grafite helm-tactics"
version="0.0.1"
archive(byte)="acic_procedural.cma"
archive(native)="acic_procedural.cmxa"
library \
acic_content \
grafite \
- acic_procedural \
content_pres \
cic_unification \
whelp \
tactics \
+ acic_procedural \
cic_disambiguation \
lexicon \
grafite_engine \
-cicClassify.cmo: cicClassify.cmi
-cicClassify.cmx: cicClassify.cmi
+proceduralClassify.cmo: proceduralClassify.cmi
+proceduralClassify.cmx: proceduralClassify.cmi
+proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
+proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
proceduralConversion.cmo: proceduralConversion.cmi
proceduralConversion.cmx: proceduralConversion.cmi
proceduralTypes.cmo: proceduralTypes.cmi
proceduralTypes.cmx: proceduralTypes.cmi
-acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
- cicClassify.cmi acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
- cicClassify.cmx acic2Procedural.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \
+ proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \
+ proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi
-cicClassify.cmo: cicClassify.cmi
-cicClassify.cmx: cicClassify.cmi
+proceduralClassify.cmo: proceduralClassify.cmi
+proceduralClassify.cmx: proceduralClassify.cmi
+proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
+proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
proceduralConversion.cmo: proceduralConversion.cmi
proceduralConversion.cmx: proceduralConversion.cmi
proceduralTypes.cmo: proceduralTypes.cmi
proceduralTypes.cmx: proceduralTypes.cmi
-acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
- cicClassify.cmi acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
- cicClassify.cmx acic2Procedural.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \
+ proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \
+ proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi
PREDICATES =
INTERFACE_FILES = \
- cicClassify.mli \
+ proceduralClassify.mli \
+ proceduralMode.mli \
proceduralConversion.mli \
proceduralTypes.mli \
acic2Procedural.mli \
module A = Cic2acic
module Ut = CicUtil
module E = CicEnvironment
+module PER = ProofEngineReduction
-module Cl = CicClassify
+module Cl = ProceduralClassify
+module M = ProceduralMode
module T = ProceduralTypes
module Cn = ProceduralConversion
let expanded_premise = "EXPANDED"
+let convert st v =
+ match get_inner_types st v with
+ | Some (st, et) ->
+ let cst, cet = cic st, cic et in
+ if PER.alpha_equivalence cst cet then [] else
+ [T.Change (st, et, "")]
+ | None -> []
+
let eta_expand n t =
let ty = C.AImplicit ("", None) in
let name i = Printf.sprintf "%s%u" expanded_premise i in
| C.AAppl (_, hd :: tl) as v ->
if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
+ let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
begin match get_inner_types st v with
- | Some (ity, _) ->
+ | Some (ity, _) when M.bkd st.context ty ->
let qs = [[T.Id ""]; mk_proof (next st) v] in
[T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | None ->
- let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+ | _ ->
let (classes, rc) as h = Cl.classify st.context ty in
let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
[T.LetIn (name, v, dtext ^ text)]
let synth = Cl.S.add 1 synth in
let qs = mk_bkd_proofs (next st) synth classes tl in
if is_rewrite_right hd then
- List.rev script @
+ List.rev script @ convert st t @
[T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
else if is_rewrite_left hd then
- List.rev script @
+ List.rev script @ convert st t @
[T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
else
let using = Some hd in
- List.rev script @
+ List.rev script @ convert st t @
[T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
| _ ->
let qs = mk_bkd_proofs (next st) synth classes tl in
let script, hd = mk_atomic st dtext hd in
- List.rev script @
+ List.rev script @ convert st t @
[T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
else
[T.Apply (t, dtext)]
+++ /dev/null
-(* Copyright (C) 2003-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-module C = Cic
-module R = CicReduction
-module D = Deannotate
-module Int = struct
- type t = int
- let compare = compare
-end
-module S = Set.Make (Int)
-
-type conclusion = (int * int) option
-
-(* debugging ****************************************************************)
-
-let string_of_entry inverse =
- if S.mem 0 inverse then "C" else
- if S.is_empty inverse then "I" else "P"
-
-let to_string (classes, rc) =
- let linearize = String.concat " " (List.map string_of_entry classes) in
- match rc with
- | None -> linearize
- | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
-
-let out_table b =
- let map i (_, inverse) =
- let map i tl = Printf.sprintf "%2u" i :: tl in
- let iset = String.concat " " (S.fold map inverse []) in
- Printf.eprintf "%2u|%s\n" i iset
- in
- Array.iteri map b;
- prerr_newline ()
-
-(****************************************************************************)
-
-let id x = x
-
-let rec list_fold_left g map = function
- | [] -> g
- | hd :: tl -> map (list_fold_left g map tl) hd
-
-let get_rels h t =
- let rec aux d g = function
- | C.Sort _
- | C.Implicit _ -> g
- | C.Rel i ->
- if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
- | C.Appl ss -> list_fold_left g (aux d) ss
- | C.Const (_, ss)
- | C.MutInd (_, _, ss)
- | C.MutConstruct (_, _, _, ss)
- | C.Var (_, ss) ->
- let map g (_, t) = aux d g t in
- list_fold_left g map ss
- | C.Meta (_, ss) ->
- let map g = function
- | None -> g
- | Some t -> aux d g t
- in
- list_fold_left g map ss
- | C.Cast (t1, t2) -> aux d (aux d g t2) t1
- | C.LetIn (_, t1, t2)
- | C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
- | C.MutCase (_, _, t1, t2, ss) ->
- aux d (aux d (list_fold_left g (aux d) ss) t2) t1
- | C.Fix (_, ss) ->
- let k = List.length ss in
- let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
- list_fold_left g map ss
- | C.CoFix (_, ss) ->
- let k = List.length ss in
- let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
- list_fold_left g map ss
- in
- let g a = a in
- aux 1 g t S.empty
-
-let split c t =
- let add s v c = Some (s, C.Decl v) :: c in
- let rec aux whd a n c = function
- | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
- | v when whd -> v :: a, n
- | v -> aux true a n c (R.whd ~delta:true c v)
- in
- aux false [] 0 c t
-
-let classify_conclusion = function
- | C.Rel i -> Some (i, 0)
- | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
- | _ -> None
-
-let classify c t =
-try
- let vs, h = split c t in
- let rc = classify_conclusion (List.hd vs) in
- let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
- let l, h = List.fold_left map ([], 0) vs in
- let b = Array.of_list (List.rev l) in
- let mk_closure b h =
- let map j = if j < h then S.union (fst b.(j)) else id in
- for i = pred h downto 0 do
- let direct, unused = b.(i) in
- b.(i) <- S.fold map direct direct, unused
- done; b
- in
- let b = mk_closure b h in
- let rec mk_inverse i direct =
- if S.is_empty direct then () else
- let j = S.choose direct in
- if j < h then
- let unused, inverse = b.(j) in
- b.(j) <- unused, S.add i inverse
- else ();
- mk_inverse i (S.remove j direct)
- in
- let map i (direct, _) = mk_inverse i direct in
- Array.iteri map b;
-(* out_table b; *)
- List.rev_map snd (List.tl (Array.to_list b)), rc
-with Invalid_argument _ -> failwith "Classify.classify"
-
-let overlaps s1 s2 =
- let predicate x = S.mem x s1 in
- S.exists predicate s2
+++ /dev/null
-(* Copyright (C) 2003-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-module S : Set.S with type elt = int
-
-type conclusion = (int * int) option
-
-val classify: Cic.context -> Cic.term -> S.t list * conclusion
-
-val to_string: S.t list * conclusion -> string
-
-val overlaps: S.t -> S.t -> bool
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module C = Cic
+module R = CicReduction
+module D = Deannotate
+module Int = struct
+ type t = int
+ let compare = compare
+end
+module S = Set.Make (Int)
+
+type conclusion = (int * int) option
+
+(* debugging ****************************************************************)
+
+let string_of_entry inverse =
+ if S.mem 0 inverse then "C" else
+ if S.is_empty inverse then "I" else "P"
+
+let to_string (classes, rc) =
+ let linearize = String.concat " " (List.map string_of_entry classes) in
+ match rc with
+ | None -> linearize
+ | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
+
+let out_table b =
+ let map i (_, inverse) =
+ let map i tl = Printf.sprintf "%2u" i :: tl in
+ let iset = String.concat " " (S.fold map inverse []) in
+ Printf.eprintf "%2u|%s\n" i iset
+ in
+ Array.iteri map b;
+ prerr_newline ()
+
+(****************************************************************************)
+
+let id x = x
+
+let rec list_fold_left g map = function
+ | [] -> g
+ | hd :: tl -> map (list_fold_left g map tl) hd
+
+let get_rels h t =
+ let rec aux d g = function
+ | C.Sort _
+ | C.Implicit _ -> g
+ | C.Rel i ->
+ if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
+ | C.Appl ss -> list_fold_left g (aux d) ss
+ | C.Const (_, ss)
+ | C.MutInd (_, _, ss)
+ | C.MutConstruct (_, _, _, ss)
+ | C.Var (_, ss) ->
+ let map g (_, t) = aux d g t in
+ list_fold_left g map ss
+ | C.Meta (_, ss) ->
+ let map g = function
+ | None -> g
+ | Some t -> aux d g t
+ in
+ list_fold_left g map ss
+ | C.Cast (t1, t2) -> aux d (aux d g t2) t1
+ | C.LetIn (_, t1, t2)
+ | C.Lambda (_, t1, t2)
+ | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+ | C.MutCase (_, _, t1, t2, ss) ->
+ aux d (aux d (list_fold_left g (aux d) ss) t2) t1
+ | C.Fix (_, ss) ->
+ let k = List.length ss in
+ let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
+ list_fold_left g map ss
+ | C.CoFix (_, ss) ->
+ let k = List.length ss in
+ let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
+ list_fold_left g map ss
+ in
+ let g a = a in
+ aux 1 g t S.empty
+
+let split c t =
+ let add s v c = Some (s, C.Decl v) :: c in
+ let rec aux whd a n c = function
+ | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
+ | v when whd -> v :: a, n
+ | v -> aux true a n c (R.whd ~delta:true c v)
+ in
+ aux false [] 0 c t
+
+let classify_conclusion = function
+ | C.Rel i -> Some (i, 0)
+ | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
+ | _ -> None
+
+let classify c t =
+try
+ let vs, h = split c t in
+ let rc = classify_conclusion (List.hd vs) in
+ let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
+ let l, h = List.fold_left map ([], 0) vs in
+ let b = Array.of_list (List.rev l) in
+ let mk_closure b h =
+ let map j = if j < h then S.union (fst b.(j)) else id in
+ for i = pred h downto 0 do
+ let direct, unused = b.(i) in
+ b.(i) <- S.fold map direct direct, unused
+ done; b
+ in
+ let b = mk_closure b h in
+ let rec mk_inverse i direct =
+ if S.is_empty direct then () else
+ let j = S.choose direct in
+ if j < h then
+ let unused, inverse = b.(j) in
+ b.(j) <- unused, S.add i inverse
+ else ();
+ mk_inverse i (S.remove j direct)
+ in
+ let map i (direct, _) = mk_inverse i direct in
+ Array.iteri map b;
+(* out_table b; *)
+ List.rev_map snd (List.tl (Array.to_list b)), rc
+with Invalid_argument _ -> failwith "Classify.classify"
+
+let overlaps s1 s2 =
+ let predicate x = S.mem x s1 in
+ S.exists predicate s2
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module S : Set.S with type elt = int
+
+type conclusion = (int * int) option
+
+val classify: Cic.context -> Cic.term -> S.t list * conclusion
+
+val to_string: S.t list * conclusion -> string
+
+val overlaps: S.t -> S.t -> bool
+
+val split: Cic.context -> Cic.term -> Cic.term list * int
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module C = Cic
+module Cl = ProceduralClassify
+
+let is_const = function
+ | C.Sort _
+ | C.Const _
+ | C.Var _
+ | C.MutInd _
+ | C.MutConstruct _ -> true
+ | _ -> false
+
+let rec is_appl b = function
+ | C.Appl (hd :: tl) -> List.fold_left is_appl (is_const hd) tl
+ | t when is_const t -> b
+ | C.Rel _ -> b
+ | _ -> false
+
+let bkd c t =
+ let ts, _ = Cl.split c t in
+ is_appl true (List.hd ts)
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val bkd: Cic.context -> Cic.term -> bool
(****************************************************************************)
-type name = string
-type what = Cic.annterm
-type how = bool
-type using = Cic.annterm
-type count = int
-type note = string
-type where = (name * name) option
+type name = string
+type what = Cic.annterm
+type how = bool
+type using = Cic.annterm
+type count = int
+type note = string
+type where = (name * name) option
+type inferred = Cic.annterm
type step = Note of note
| Theorem of name * what * note
| Elim of what * using option * note
| Apply of what * note
| Whd of count * note
+ | Change of inferred * what * note
| Branch of step list list * note
(* annterm constructors *****************************************************)
let tactic = G.Reduce (floc, `Whd, pattern) in
mk_tactic tactic
+let mk_change t =
+ let pattern = None, [], Some hole in
+ let tactic = G.Change (floc, pattern, t) in
+ mk_tactic tactic
+
let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
| Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
| Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
| Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a)
+ | Change (t, _, s) -> mk_note s :: cont sep (mk_change t :: a)
| Branch ([], s) -> a
| Branch ([ps], s) -> render_steps sep a ps
| Branch (pss, s) ->
(****************************************************************************)
-type name = string
-type what = Cic.annterm
-type how = bool
-type using = Cic.annterm
-type count = int
-type note = string
-type where = (name * name) option
+type name = string
+type what = Cic.annterm
+type how = bool
+type using = Cic.annterm
+type count = int
+type note = string
+type where = (name * name) option
+type inferred = Cic.annterm
type step = Note of note
| Theorem of name * what * note
| Elim of what * using option * note
| Apply of what * note
| Whd of count * note
+ | Change of inferred * what * note
| Branch of step list list * note
val render_steps:
- (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list ->
+ (what, inferred, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list ->
step list ->
- (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list
+ (what, inferred, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list
val count_steps:
int -> step list -> int
id, Some typ
| arg = single_arg -> arg, None
| SYMBOL "_" -> Ast.Ident ("_", None), None
+ | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
+ Ast.Ident ("_", None), Some typ
]
];
match_pattern: [
mk_tactic (exact_tac ~term)
(* not really "primitive" tactics .... *)
-let elim_tac ~term =
- let elim_tac ~term (proof, goal) =
+let elim_tac ?using ~term =
+ let elim_tac (proof, goal) =
let module T = CicTypeChecker in
let module U = UriManager in
let module R = CicReduction in
in
U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
in
- let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
+ let eliminator_ref = match using with
+ | None -> C.Const (eliminator_uri,exp_named_subst)
+ | Some t -> t
+ in
let ety,_ =
T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
let rec find_args_no =
in
proof'', patched_new_goals
in
- mk_tactic (elim_tac ~term)
+ mk_tactic elim_tac
;;
let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ~term:what)
+ Tacticals.then_ ~start:(elim_tac ?using ~term:what)
~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
;;
(* The simplification is performed only on the conclusion *)
let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ~term:what)
+ Tacticals.then_ ~start:(elim_tac ?using ~term:what)
~continuation:
(Tacticals.thens
~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
projects / helm.git / commitdiff