aboutsummaryrefslogtreecommitdiff
path: root/plugins/interface
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/interface')
-rw-r--r--plugins/interface/blast.ml282
-rw-r--r--plugins/interface/centaur.ml458
-rw-r--r--plugins/interface/coqparser.ml70
-rw-r--r--plugins/interface/dad.ml32
-rw-r--r--plugins/interface/debug_tac.ml446
-rw-r--r--plugins/interface/depends.ml4
-rw-r--r--plugins/interface/history.ml50
-rwxr-xr-xplugins/interface/line_parser.ml424
-rw-r--r--plugins/interface/name_to_ast.ml46
-rw-r--r--plugins/interface/paths.ml2
-rw-r--r--plugins/interface/pbp.ml120
-rw-r--r--plugins/interface/showproof.ml264
-rw-r--r--plugins/interface/showproof_ct.ml24
-rw-r--r--plugins/interface/translate.ml12
-rw-r--r--plugins/interface/xlate.ml368
15 files changed, 701 insertions, 701 deletions
diff --git a/plugins/interface/blast.ml b/plugins/interface/blast.ml
index 2f0095a56c..55db032f30 100644
--- a/plugins/interface/blast.ml
+++ b/plugins/interface/blast.ml
@@ -71,11 +71,11 @@ let free_try tac g =
else (failwith "not free")
;;
let adrel (x,t) e =
- match x with
+ match x with
Name(xid) -> Environ.push_rel (x,None,t) e
| Anonymous -> Environ.push_rel (x,None,t) e
(* les constantes ayant une définition apparaissant dans x *)
-let rec def_const_in_term_rec vl x =
+let rec def_const_in_term_rec vl x =
match (kind_of_term x) with
Prod(n,t,c)->
let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
@@ -89,7 +89,7 @@ let rec def_const_in_term_rec vl x =
new_sort_in_family (inductive_sort_family mip)
| Construct(c) ->
def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
- | Case(_,x,t,a)
+ | Case(_,x,t,a)
-> def_const_in_term_rec vl x
| Cast(x,_,t)-> def_const_in_term_rec vl t
| Const(c) -> def_const_in_term_rec vl (Typeops.type_of_constant vl c)
@@ -99,7 +99,7 @@ let def_const_in_term_ x =
def_const_in_term_rec (Global.env()) (strip_outer_cast x)
;;
(*************************************************************************
- recopiés de refiner.ml, car print_subscript pas exportée dans refiner.mli
+ recopiés de refiner.ml, car print_subscript pas exportée dans refiner.mli
modif de print_info_script avec pr_bar
*)
@@ -115,9 +115,9 @@ let rec print_info_script sigma osign pf =
| [] ->
(str " " ++ fnl())
| [pf1] ->
- if pf1.ref = None then
+ if pf1.ref = None then
(str " " ++ fnl())
- else
+ else
(str";" ++ brk(1,3) ++
print_info_script sigma sign pf1)
| _ -> ( str";[" ++ fnl() ++
@@ -125,11 +125,11 @@ let rec print_info_script sigma osign pf =
(print_info_script sigma sign) spfl ++
str"]")
-let format_print_info_script sigma osign pf =
+let format_print_info_script sigma osign pf =
hov 0 (print_info_script sigma osign pf)
-
-let print_subscript sigma sign pf =
- (* if is_tactic_proof pf then
+
+let print_subscript sigma sign pf =
+ (* if is_tactic_proof pf then
format_print_info_script sigma sign (subproof_of_proof pf)
else *)
format_print_info_script sigma sign pf
@@ -150,98 +150,98 @@ let pp_string x =
let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
-let unify_e_resolve (c,clenv) gls =
+let unify_e_resolve (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
let _ = clenv_unique_resolver false clenv' gls in
Hiddentac.h_simplest_eapply c gls
let rec e_trivial_fail_db db_list local_db goal =
- let tacl =
+ let tacl =
registered_e_assumption ::
- (tclTHEN Tactics.intro
+ (tclTHEN Tactics.intro
(function g'->
let d = pf_last_hyp g' in
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db db_list
(Hint_db.add_list hintl local_db) g'))) ::
(List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
- in
- tclFIRST (List.map tclCOMPLETE tacl) goal
+ in
+ tclFIRST (List.map tclCOMPLETE tacl) goal
-and e_my_find_search db_list local_db hdc concl =
+and e_my_find_search db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
let hintl =
- if occur_existential concl then
- list_map_append (fun db ->
+ if occur_existential concl then
+ list_map_append (fun db ->
let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
- else
- list_map_append (fun db ->
+ else
+ list_map_append (fun db ->
let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
- in
- let tac_of_hint =
- fun (st, ({pri=b; pat = p; code=t} as _patac)) ->
- (b,
+ in
+ let tac_of_hint =
+ fun (st, ({pri=b; pat = p; code=t} as _patac)) ->
+ (b,
let tac =
match t with
| Res_pf (term,cl) -> unify_resolve st (term,cl)
| ERes_pf (term,cl) -> unify_e_resolve (term,cl)
| Give_exact (c) -> e_give_exact c
| Res_pf_THEN_trivial_fail (term,cl) ->
- tclTHEN (unify_e_resolve (term,cl))
+ tclTHEN (unify_e_resolve (term,cl))
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> unfold_in_concl [all_occurrences,c]
| Extern tacast -> Auto.conclPattern concl p tacast
- in
+ in
(free_try tac,pr_autotactic t))
(*i
- fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
+ fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
try tac gls
- with e when Logic.catchable_exception(e) ->
- (Format.print_string "Fail\n";
- Format.print_flush ();
+ with e when Logic.catchable_exception(e) ->
+ (Format.print_string "Fail\n";
+ Format.print_flush ();
raise e)
i*)
- in
+ in
List.map tac_of_hint hintl
-
-and e_trivial_resolve db_list local_db gl =
- try
- priority
- (e_my_find_search db_list local_db
+
+and e_trivial_resolve db_list local_db gl =
+ try
+ priority
+ (e_my_find_search db_list local_db
(fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let e_possible_resolve db_list local_db gl =
- try List.map snd (e_my_find_search db_list local_db
+ try List.map snd (e_my_find_search db_list local_db
(fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let assumption_tac_list id = apply_tac_list (e_give_exact (mkVar id))
-let find_first_goal gls =
+let find_first_goal gls =
try first_goal gls with UserError _ -> assert false
(*s The following module [SearchProblem] is used to instantiate the generic
exploration functor [Explore.Make]. *)
-
+
module MySearchProblem = struct
- type state = {
+ type state = {
depth : int; (*r depth of search before failing *)
tacres : goal list sigma * validation;
last_tactic : std_ppcmds;
dblist : Auto.hint_db list;
localdb : Auto.hint_db list }
-
+
let success s = (sig_it (fst s.tacres)) = []
let rec filter_tactics (glls,v) = function
| [] -> []
- | (tac,pptac) :: tacl ->
- try
- let (lgls,ptl) = apply_tac_list tac glls in
+ | (tac,pptac) :: tacl ->
+ try
+ let (lgls,ptl) = apply_tac_list tac glls in
let v' p = v (ptl p) in
((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
with e when Logic.catchable_exception e ->
@@ -254,18 +254,18 @@ module MySearchProblem = struct
let nbgoals s = List.length (sig_it (fst s.tacres)) in
if d <> 0 then d else nbgoals s - nbgoals s'
- let branching s =
- if s.depth = 0 then
+ let branching s =
+ if s.depth = 0 then
[]
- else
+ else
let lg = fst s.tacres in
let nbgl = List.length (sig_it lg) in
assert (nbgl > 0);
let g = find_first_goal lg in
- let assumption_tacs =
- let l =
+ let assumption_tacs =
+ let l =
filter_tactics s.tacres
- (List.map
+ (List.map
(fun id -> (e_give_exact (mkVar id),
(str "Exact" ++ spc()++ pr_id id)))
(pf_ids_of_hyps g))
@@ -274,40 +274,40 @@ module MySearchProblem = struct
last_tactic = pp; dblist = s.dblist;
localdb = List.tl s.localdb }) l
in
- let intro_tac =
- List.map
- (fun ((lgls,_) as res,pp) ->
- let g' = first_goal lgls in
- let hintl =
+ let intro_tac =
+ List.map
+ (fun ((lgls,_) as res,pp) ->
+ let g' = first_goal lgls in
+ let hintl =
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
in
let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
- { depth = s.depth; tacres = res;
+ { depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
localdb = ldb :: List.tl s.localdb })
(filter_tactics s.tacres [Tactics.intro,(str "Intro" )])
in
- let rec_tacs =
- let l =
+ let rec_tacs =
+ let l =
filter_tactics s.tacres
(e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
in
- List.map
- (fun ((lgls,_) as res, pp) ->
+ List.map
+ (fun ((lgls,_) as res, pp) ->
let nbgl' = List.length (sig_it lgls) in
if nbgl' < nbgl then
{ depth = s.depth; tacres = res; last_tactic = pp;
dblist = s.dblist; localdb = List.tl s.localdb }
- else
- { depth = pred s.depth; tacres = res;
+ else
+ { depth = pred s.depth; tacres = res;
dblist = s.dblist; last_tactic = pp;
- localdb =
+ localdb =
list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
l
in
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
- let pp s =
+ let pp s =
msg (hov 0 (str " depth="++ int s.depth ++ spc() ++
s.last_tactic ++ str "\n"))
@@ -331,31 +331,31 @@ let e_depth_search debug p db_list local_db gl =
let e_breadth_search debug n db_list local_db gl =
try
- let tac =
- if debug then MySearch.debug_breadth_first else MySearch.breadth_first
+ let tac =
+ if debug then MySearch.debug_breadth_first else MySearch.breadth_first
in
let s = tac (make_initial_state n gl db_list local_db) in
s.MySearchProblem.tacres
with Not_found -> error "EAuto: breadth first search failed"
-let e_search_auto debug (n,p) db_list gl =
- let local_db = make_local_hint_db true [] gl in
- if n = 0 then
+let e_search_auto debug (n,p) db_list gl =
+ let local_db = make_local_hint_db true [] gl in
+ if n = 0 then
e_depth_search debug p db_list local_db gl
- else
+ else
e_breadth_search debug n db_list local_db gl
-let eauto debug np dbnames =
+let eauto debug np dbnames =
let db_list =
List.map
- (fun x ->
+ (fun x ->
try searchtable_map x
with Not_found -> error ("EAuto: "^x^": No such Hint database"))
- ("core"::dbnames)
+ ("core"::dbnames)
in
tclTRY (e_search_auto debug np db_list)
-let full_eauto debug n gl =
+let full_eauto debug n gl =
let dbnames = current_db_names () in
let dbnames = list_subtract dbnames ["v62"] in
let db_list = List.map searchtable_map dbnames in
@@ -373,49 +373,49 @@ let my_full_eauto n gl = full_eauto false (n,0) gl
de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
let rec trivial_fail_db db_list local_db gl =
- let intro_tac =
- tclTHEN intro
+ let intro_tac =
+ tclTHEN intro
(fun g'->
let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
in
- tclFIRST
+ tclFIRST
(assumption::intro_tac::
- (List.map tclCOMPLETE
+ (List.map tclCOMPLETE
(trivial_resolve db_list local_db (pf_concl gl)))) gl
and my_find_search db_list local_db hdc concl =
- let tacl =
- if occur_existential concl then
- list_map_append (fun db ->
+ let tacl =
+ if occur_existential concl then
+ list_map_append (fun db ->
let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
- else
- list_map_append (fun db ->
+ else
+ list_map_append (fun db ->
let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
- List.map
- (fun (st, {pri=b; pat=p; code=t} as _patac) ->
+ List.map
+ (fun (st, {pri=b; pat=p; code=t} as _patac) ->
(b,
match t with
| Res_pf (term,cl) -> unify_resolve st (term,cl)
| ERes_pf (_,c) -> (fun gl -> error "eres_pf")
| Give_exact c -> exact_check c
- | Res_pf_THEN_trivial_fail (term,cl) ->
- tclTHEN
- (unify_resolve st (term,cl))
+ | Res_pf_THEN_trivial_fail (term,cl) ->
+ tclTHEN
+ (unify_resolve st (term,cl))
(trivial_fail_db db_list local_db)
| Unfold_nth c -> unfold_in_concl [all_occurrences,c]
| Extern tacast -> conclPattern concl p tacast))
tacl
-and trivial_resolve db_list local_db cl =
- try
+and trivial_resolve db_list local_db cl =
+ try
let hdconstr = fst (head_constr_bound cl) in
- priority
+ priority
(my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
- with Bound | Not_found ->
+ with Bound | Not_found ->
[]
(**************************************************************************)
@@ -423,88 +423,88 @@ and trivial_resolve db_list local_db cl =
(**************************************************************************)
let possible_resolve db_list local_db cl =
- try
+ try
let hdconstr = fst (head_constr_bound cl) in
- List.map snd
+ List.map snd
(my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
- with Bound | Not_found ->
+ with Bound | Not_found ->
[]
-let decomp_unary_term c gls =
- let typc = pf_type_of gls c in
- let t = head_constr typc in
- if Hipattern.is_conjunction (applist t) then
- simplest_case c gls
- else
+let decomp_unary_term c gls =
+ let typc = pf_type_of gls c in
+ let t = head_constr typc in
+ if Hipattern.is_conjunction (applist t) then
+ simplest_case c gls
+ else
errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
-let decomp_empty_term c gls =
- let typc = pf_type_of gls c in
- let (hd,_) = decompose_app typc in
- if Hipattern.is_empty_type hd then
- simplest_case c gls
- else
+let decomp_empty_term c gls =
+ let typc = pf_type_of gls c in
+ let (hd,_) = decompose_app typc in
+ if Hipattern.is_empty_type hd then
+ simplest_case c gls
+ else
errorlabstrm "Auto.decomp_empty_term" (str "not an empty type")
-(* decomp is an natural number giving an indication on decomposition
+(* decomp is an natural number giving an indication on decomposition
of conjunction in hypotheses, 0 corresponds to no decomposition *)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
let rec search_gen decomp n db_list local_db extra_sign goal =
if n=0 then error "BOUND 2";
- let decomp_tacs = match decomp with
- | 0 -> []
- | p ->
+ let decomp_tacs = match decomp with
+ | 0 -> []
+ | p ->
(tclFIRST_PROGRESS_ON decomp_empty_term extra_sign)
::
- (List.map
- (fun id -> tclTHEN (decomp_unary_term (mkVar id))
- (tclTHEN
+ (List.map
+ (fun id -> tclTHEN (decomp_unary_term (mkVar id))
+ (tclTHEN
(clear [id])
(free_try (search_gen decomp p db_list local_db []))))
- (pf_ids_of_hyps goal))
+ (pf_ids_of_hyps goal))
in
- let intro_tac =
- tclTHEN intro
- (fun g' ->
+ let intro_tac =
+ tclTHEN intro
+ (fun g' ->
let (hid,_,htyp) = pf_last_hyp g' in
- let hintl =
- try
+ let hintl =
+ try
[make_apply_entry (pf_env g') (project g')
- (true,true,false)
+ (true,true,false)
None
(mkVar hid,htyp)]
- with Failure _ -> []
+ with Failure _ -> []
in
(free_try
(search_gen decomp n db_list (Hint_db.add_list hintl local_db)
[mkVar hid])
g'))
in
- let rec_tacs =
- List.map
- (fun ntac ->
+ let rec_tacs =
+ List.map
+ (fun ntac ->
tclTHEN ntac
(free_try
(search_gen decomp (n-1) db_list local_db [])))
(possible_resolve db_list local_db (pf_concl goal))
- in
+ in
tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
let search = search_gen 0
let default_search_depth = ref 5
-
-let full_auto n gl =
+
+let full_auto n gl =
let dbnames = current_db_names () in
let dbnames = list_subtract dbnames ["v62"] in
let db_list = List.map searchtable_map dbnames in
let hyps = List.map mkVar (pf_ids_of_hyps gl) in
tclTRY (search n db_list (make_local_hint_db false [] gl) hyps) gl
-
+
let default_full_auto gl = full_auto !default_search_depth gl
(************************************************************************)
@@ -518,15 +518,15 @@ let blast_auto = (free_try default_full_auto)
;;
let blast_simpl = (free_try (reduce (Simpl None) onConcl))
;;
-let blast_induction1 =
+let blast_induction1 =
(free_try (tclTHEN (tclTRY intro)
(tclTRY (onLastHyp simplest_elim))))
;;
-let blast_induction2 =
+let blast_induction2 =
(free_try (tclTHEN (tclTRY (tclTHEN intro intro))
(tclTRY (onLastHyp simplest_elim))))
;;
-let blast_induction3 =
+let blast_induction3 =
(free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro)))
(tclTRY (onLastHyp simplest_elim))))
;;
@@ -554,7 +554,7 @@ let vire_extvar s =
if get s i = '?'
then (interro := true;
interro_pos := i)
- else if (!interro &&
+ else if (!interro &&
(List.mem (get s i)
['0';'1';'2';'3';'4';'5';'6';'7';'8';'9']))
then set s i ' '
@@ -570,13 +570,13 @@ let blast gls =
ref = None } in
try (let (sgl,v) as _res = !blast_tactic gls in
let {it=lg} = sgl in
- if lg = []
+ if lg = []
then (let pf = v (List.map leaf (sig_it sgl)) in
let sign = (sig_it gls).evar_hyps in
- let x = print_subscript
+ let x = print_subscript
(sig_sig gls) sign pf in
msgnl (hov 0 (str"Blast ==> " ++ x));
- let x = print_subscript
+ let x = print_subscript
(sig_sig gls) sign pf in
let tac_string =
pp_string (hov 0 x ) in
@@ -589,15 +589,15 @@ let blast gls =
with _ -> failwith "echec de blast"
;;
-let blast_tac display_function = function
- | (n::_) as _l ->
+let blast_tac display_function = function
+ | (n::_) as _l ->
(function g ->
let exp_ast = (blast g) in
(display_function exp_ast;
tclIDTAC g))
| _ -> failwith "expecting other arguments";;
-let blast_tac_txt =
+let blast_tac_txt =
blast_tac
(function x -> msgnl(Pptactic.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
@@ -621,8 +621,8 @@ CAMLLIB=/usr/local/lib/ocaml
CAMLP4LIB=/usr/local/lib/camlp4
export CAMLLIB
export COQTOP
-export CAMLP4LIB
-d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe
+export CAMLP4LIB
+d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe
Drop.
#use "/cygdrive/D/Tools/coq-7.0-3mai/dev/base_include";;
*)
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index ee46cef8b2..e7084fbb00 100644
--- a/plugins/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
@@ -74,17 +74,17 @@ let pcoq_history = ref true;;
let assert_pcoq_history f a =
if !pcoq_history then f a else error "Pcoq-style history tracking deactivated";;
-let current_proof_name () =
- try
+let current_proof_name () =
+ try
string_of_id (get_current_proof_name ())
with
UserError("Pfedit.get_proof", _) -> "";;
let current_goal_index = ref 0;;
-let guarded_force_eval_stream (s : std_ppcmds) =
+let guarded_force_eval_stream (s : std_ppcmds) =
let l = ref [] in
- let f elt = l:= elt :: !l in
+ let f elt = l:= elt :: !l in
(try Stream.iter f s with
| _ -> f (Stream.next (str "error guarded_force_eval_stream")));
Stream.of_list (List.rev !l);;
@@ -118,7 +118,7 @@ type vtp_tree =
| P_text of ct_TEXT
| P_ids of ct_ID_LIST;;
-let print_tree t =
+let print_tree t =
(match t with
| P_rl x -> fRULE_LIST x
| P_r x -> fRULE x
@@ -138,10 +138,10 @@ let ctf_header message_name request_id =
int request_id ++ fnl();;
let ctf_acknowledge_command request_id command_count opt_exn =
- let goal_count, goal_index =
+ let goal_count, goal_index =
if refining() then
let g_count =
- List.length
+ List.length
(fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in
g_count, !current_goal_index
else
@@ -192,7 +192,7 @@ let ctf_AbortedAllMessage () =
fnl() ++ str "message" ++ fnl() ++ str "aborted_all" ++ fnl();;
let ctf_AbortedMessage request_id na =
- ctf_header "aborted_proof" request_id ++ str na ++ fnl () ++
+ ctf_header "aborted_proof" request_id ++ str na ++ fnl () ++
str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
let ctf_UserErrorMessage request_id stream =
@@ -256,7 +256,7 @@ let show_nth n =
++ pr_nth_open_subgoal n)
None
with
- | Invalid_argument s ->
+ | Invalid_argument s ->
error "No focused proof (No proof-editing in progress)";;
let show_subgoals () =
@@ -265,7 +265,7 @@ let show_subgoals () =
++ pr_open_subgoals ())
None
with
- | Invalid_argument s ->
+ | Invalid_argument s ->
error "No focused proof (No proof-editing in progress)";;
(* The rest of the file contains commands that are changed from the plain
@@ -280,11 +280,11 @@ let filter_by_module_from_varg_list l =
*)
let add_search (global_reference:global_reference) assumptions cstr =
- try
+ try
let id_string =
string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty
global_reference) in
- let ast =
+ let ast =
try
CT_premise (CT_ident id_string, translate_constr false assumptions cstr)
with Not_found ->
@@ -324,20 +324,20 @@ let ct_print_eval red_fun env evmap ast judg =
translate_constr false env ntyp)]));;
let pbp_tac_pcoq =
- pbp_tac (function (x:raw_tactic_expr) ->
+ pbp_tac (function (x:raw_tactic_expr) ->
output_results
(ctf_header "pbp_results" !global_request_id)
(Some (P_t(xlate_tactic x))));;
let blast_tac_pcoq =
- blast_tac (function (x:raw_tactic_expr) ->
+ blast_tac (function (x:raw_tactic_expr) ->
output_results
(ctf_header "pbp_results" !global_request_id)
(Some (P_t(xlate_tactic x))));;
-(* <\cpa>
+(* <\cpa>
let dad_tac_pcoq =
- dad_tac(function x ->
+ dad_tac(function x ->
output_results
(ctf_header "pbp_results" !global_request_id)
(Some (P_t(xlate_tactic x))));;
@@ -368,7 +368,7 @@ Caution, this is in the middle of what looks like dead code. ;
e ->
match !the_goal with
None -> raise e
- | Some g ->
+ | Some g ->
(output_results
(ctf_Location !global_request_id)
(Some (P_s_int
@@ -376,7 +376,7 @@ Caution, this is in the middle of what looks like dead code. ;
(List.map
(fun n -> CT_coerce_INT_to_SIGNED_INT
(CT_int n))
- (clean_path tac
+ (clean_path tac
(List.rev !the_path)))))));
(output_results
(ctf_OtherGoal !global_request_id)
@@ -417,7 +417,7 @@ let inspect n =
add_search2 (Nametab.locate (qualid_of_path sp))
(Pretyping.Default.understand Evd.empty (Global.env())
(RRef(dummy_loc, IndRef(kn,0))))
- | _ -> failwith ("unexpected value 1 for "^
+ | _ -> failwith ("unexpected value 1 for "^
(string_of_id (basename (fst oname)))))
| _ -> failwith "unexpected value")
with e -> ())
@@ -427,7 +427,7 @@ let inspect n =
(Some
(P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));;
-let ct_int_to_TARG n =
+let ct_int_to_TARG n =
CT_coerce_FORMULA_OR_INT_to_TARG
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
(CT_coerce_INT_to_ID_OR_INT (CT_int n)));;
@@ -561,7 +561,7 @@ let pcoq_search s l =
*)
ctv_SEARCH_LIST:=[];
begin match s with
- | SearchAbout sl ->
+ | SearchAbout sl ->
raw_search_about (filter_by_module_from_list l) add_search
(List.map (on_snd interp_search_about_item) sl)
| SearchPattern c ->
@@ -580,7 +580,7 @@ let pcoq_search s l =
let rec hyp_pattern_filter pat name a c =
let _c1 = strip_outer_cast c in
match kind_of_term c with
- | Prod(_, hyp, c2) ->
+ | Prod(_, hyp, c2) ->
(try
(* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
let _ = msgnl ((str "PAT ") ++ (Printer.pr_constr_pattern pat)) in *)
@@ -605,7 +605,7 @@ let hyp_search_pattern c l =
(Some
(P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));;
let pcoq_print_name ref =
- output_results
+ output_results
(fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl () ++ print_name ref )
None
@@ -665,8 +665,8 @@ let pcoq_print_object_template object_to_ast_list sp =
(* This function mirror what print_check does *)
let pcoq_print_typed_value_in_env env (value, typ) =
- let value_ct_ast =
- (try translate_constr false (Global.env()) value
+ let value_ct_ast =
+ (try translate_constr false (Global.env()) value
with UserError(f,str) ->
raise(UserError(f,Printer.pr_lconstr value ++
fnl () ++ str ))) in
@@ -797,7 +797,7 @@ let start_depends_dumps () = gen_start_depends_dumps output_depends output_depen
let start_depends_dumps_debug () = gen_start_depends_dumps print_depends print_depends print_depends print_depends
TACTIC EXTEND pbp
-| [ "pbp" ident_opt(idopt) natural_list(nl) ] ->
+| [ "pbp" ident_opt(idopt) natural_list(nl) ] ->
[ if_pcoq pbp_tac_pcoq idopt nl ]
END
@@ -810,10 +810,10 @@ TACTIC EXTEND ct_debugtac2
END
-let start_pcoq_mode debug =
+let start_pcoq_mode debug =
begin
pcoq_started := Some debug;
-(* <\cpa>
+(* <\cpa>
start_dad();
</cpa> *)
(* The following ones are added to enable rich comments in pcoq *)
@@ -830,7 +830,7 @@ let start_pcoq_mode debug =
*)
set_pcoq_hook pcoq_hook;
start_pcoq_objects();
- Flags.print_emacs := false; Pp.make_pp_nonemacs();
+ Flags.print_emacs := false; Pp.make_pp_nonemacs();
end;;
diff --git a/plugins/interface/coqparser.ml b/plugins/interface/coqparser.ml
index df5e66b50f..730af3ca2f 100644
--- a/plugins/interface/coqparser.ml
+++ b/plugins/interface/coqparser.ml
@@ -53,13 +53,13 @@ let execute_when_necessary v =
(match v with
| VernacOpenCloseScope sc -> Vernacentries.interp v
| VernacRequire (_,_,l) ->
- (try
+ (try
Vernacentries.interp v
with _ ->
let l=prlist_with_sep spc pr_reference l in
msgnl (str "Reinterning of " ++ l ++ str " failed"))
| VernacRequireFrom (_,_,f) ->
- (try
+ (try
Vernacentries.interp v
with _ ->
msgnl (str "Reinterning of " ++ Util.pr_str f ++ str " failed"))
@@ -112,7 +112,7 @@ let rec get_sub_aux string_list snd_pos =
let rec get_substring_list string_list fst_pos snd_pos =
match string_list with
[] -> []
- | s::l ->
+ | s::l ->
let len = String.length s in
if fst_pos > len then
get_substring_list l (fst_pos - len - 1) (snd_pos - len - 1)
@@ -146,10 +146,10 @@ let make_parse_error_item s l =
let parse_command_list reqid stream string_list =
let rec parse_whole_stream () =
let this_pos = Stream.count stream in
- let first_ast =
+ let first_ast =
try ParseOK (Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
with
- | (Stdpp.Exc_located(l, Stream.Error txt)) as e ->
+ | (Stdpp.Exc_located(l, Stream.Error txt)) as e ->
begin
msgnl (ctf_SyntaxWarningMessage reqid (Cerrors.explain_exn e));
try
@@ -161,7 +161,7 @@ let parse_command_list reqid stream string_list =
(Stream.count stream))
with End_of_file -> ParseOK None
end
- | e->
+ | e->
begin
discard_to_dot stream;
ParseError ("PARSING_ERROR2",
@@ -172,11 +172,11 @@ let parse_command_list reqid stream string_list =
let _ast0 = (execute_when_necessary ast) in
(try xlate_vernac ast
with e ->
- make_parse_error_item "PARSING_ERROR2"
+ make_parse_error_item "PARSING_ERROR2"
(get_substring_list string_list this_pos
(Stream.count stream)))::parse_whole_stream()
| ParseOK None -> []
- | ParseError (s,l) ->
+ | ParseError (s,l) ->
(make_parse_error_item s l)::parse_whole_stream()
in
match parse_whole_stream () with
@@ -200,21 +200,21 @@ let parse_string_action reqid phylum char_stream string_list =
(Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream))))
| "TACTIC_COM" ->
P_t
- (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi
+ (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi
(Gram.parsable char_stream)))
| "FORMULA" ->
P_f
(xlate_formula
- (Gram.Entry.parse
+ (Gram.Entry.parse
(Pcoq.eoi_entry Pcoq.Constr.lconstr) (Gram.parsable char_stream)))
| "ID" -> P_id (CT_ident
- (Libnames.string_of_qualid
- (snd
+ (Libnames.string_of_qualid
+ (snd
(Gram.Entry.parse (Pcoq.eoi_entry Pcoq.Prim.qualid)
(Gram.parsable char_stream)))))
| "STRING" ->
P_s
- (CT_string (Gram.Entry.parse Pcoq.Prim.string
+ (CT_string (Gram.Entry.parse Pcoq.Prim.string
(Gram.parsable char_stream)))
| "INT" ->
P_i (CT_int (Gram.Entry.parse Pcoq.Prim.natural
@@ -225,7 +225,7 @@ let parse_string_action reqid phylum char_stream string_list =
| Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
flush_until_end_of_stream char_stream;
msgnl (ctf_SyntaxErrorMessage reqid
- (Cerrors.explain_exn
+ (Cerrors.explain_exn
(Stdpp.Exc_located(l,Stream.Error "match failure"))))
| e ->
flush_until_end_of_stream char_stream;
@@ -233,7 +233,7 @@ let parse_string_action reqid phylum char_stream string_list =
let quiet_parse_string_action char_stream =
- try let _ =
+ try let _ =
Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
()
with
@@ -242,9 +242,9 @@ let quiet_parse_string_action char_stream =
let parse_file_action reqid file_name =
try let file_chan = open_in file_name in
- (* file_chan_err, stream_err are the channel and stream used to
+ (* file_chan_err, stream_err are the channel and stream used to
get the text when a syntax error occurs *)
- let file_chan_err = open_in file_name in
+ let file_chan_err = open_in file_name in
let stream = Stream.of_channel file_chan in
let _stream_err = Stream.of_channel file_chan_err in
let rec discard_to_dot () =
@@ -252,21 +252,21 @@ let parse_file_action reqid file_name =
with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in
match let rec parse_whole_file () =
let this_pos = Stream.count stream in
- match
+ match
try
ParseOK(Gram.Entry.parse Pcoq.main_entry (Gram.parsable stream))
with
- | Stdpp.Exc_located(l,Stream.Error txt) ->
+ | Stdpp.Exc_located(l,Stream.Error txt) ->
msgnl (ctf_SyntaxWarningMessage reqid
(str "Error with file" ++ spc () ++
str file_name ++ fnl () ++
- Cerrors.explain_exn
+ Cerrors.explain_exn
(Stdpp.Exc_located(l,Stream.Error txt))));
- (try
+ (try
begin
discard_to_dot ();
ParseError ("PARSING_ERROR",
- (make_string_list file_chan_err this_pos
+ (make_string_list file_chan_err this_pos
(Stream.count stream)))
end
with End_of_file -> ParseOK None)
@@ -277,10 +277,10 @@ let parse_file_action reqid file_name =
(make_string_list file_chan this_pos
(Stream.count stream)))
end
-
+
with
| ParseOK (Some (_,ast)) ->
- let _ast0=(execute_when_necessary ast) in
+ let _ast0=(execute_when_necessary ast) in
let term =
(try xlate_vernac ast
with e ->
@@ -291,10 +291,10 @@ let parse_file_action reqid file_name =
"\n");
make_parse_error_item "PARSING_ERROR2"
(make_string_list file_chan_err this_pos
- (Stream.count stream))) in
+ (Stream.count stream))) in
term::parse_whole_file ()
| ParseOK None -> []
- | ParseError (s,l) ->
+ | ParseError (s,l) ->
(make_parse_error_item s l)::parse_whole_file () in
parse_whole_file () with
| first_one :: tail ->
@@ -305,7 +305,7 @@ let parse_file_action reqid file_name =
| Stdpp.Exc_located(l,Match_failure(_,_,_)) ->
msgnl
(ctf_SyntaxErrorMessage reqid
- (str "Error with file" ++ spc () ++ str file_name ++
+ (str "Error with file" ++ spc () ++ str file_name ++
fnl () ++
Cerrors.explain_exn
(Stdpp.Exc_located(l,Stream.Error "match failure"))))
@@ -320,7 +320,7 @@ let add_rec_path_action reqid string_arg ident_arg =
begin
add_rec_path directory_name (Libnames.dirpath_of_string ident_arg)
end;;
-
+
let add_path_action reqid string_arg =
let directory_name = expand_path_macros string_arg in
@@ -338,7 +338,7 @@ let load_syntax_action reqid module_name =
(let qid = Libnames.qualid_of_ident (Names.id_of_string module_name) in
require_library [dummy_loc,qid] None;
msg (str "opening... ");
- Declaremods.import_module false (Nametab.locate_module qid);
+ Declaremods.import_module false (Nametab.locate_module qid);
msgnl (str "done" ++ fnl ());
())
with
@@ -365,11 +365,11 @@ let coqparser_loop inchan =
add_path_action, add_rec_path_action, load_syntax_action) inchan;;
if !Sys.interactive then ()
- else
+ else
Libobject.relax true;
-(let coqdir =
+(let coqdir =
try Sys.getenv "COQDIR"
- with Not_found ->
+ with Not_found ->
let coqdir = Envars.coqlib () in
if Sys.file_exists coqdir then
coqdir
@@ -385,8 +385,8 @@ Libobject.relax true;
try
Sys.getenv "VERNACRC"
with
- Not_found ->
- List.fold_left
+ Not_found ->
+ List.fold_left
(fun s1 s2 -> (Filename.concat s1 s2))
coqdir [ "plugins"; "interface"; "vernacrc"] in
try
@@ -417,6 +417,6 @@ Libobject.relax true;
msgnl (str "Starting Centaur Specialized Parser Loop");
try
coqparser_loop stdin
-with
+with
| End_of_file -> ()
| e -> msgnl(Cerrors.explain_exn e))
diff --git a/plugins/interface/dad.ml b/plugins/interface/dad.ml
index c2ab2dc8d0..fb0562c571 100644
--- a/plugins/interface/dad.ml
+++ b/plugins/interface/dad.ml
@@ -58,9 +58,9 @@ let zz = Util.dummy_loc;;
let rec get_subterm (depth:int) (path: int list) (constr:constr) =
match depth, path, kind_of_term constr with
0, l, c -> (constr,l)
- | n, 2::a::tl, App(func,arr) ->
+ | n, 2::a::tl, App(func,arr) ->
get_subterm (n - 2) tl arr.(a-1)
- | _,l,_ -> failwith (int_list_to_string
+ | _,l,_ -> failwith (int_list_to_string
"wrong path or wrong form of term"
l);;
@@ -93,12 +93,12 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
if deg > length then
failwith "internal"
else
- let term_to_match, p_r =
- try
+ let term_to_match, p_r =
+ try
get_subterm (length - deg) p constr
with
Failure s -> failwith "internal" in
- let _, constr_pat =
+ let _, constr_pat =
intern_constr_pattern Evd.empty (Global.env())
((*ct_to_ast*) pat) in
let subst = matches constr_pat term_to_match in
@@ -136,26 +136,26 @@ let dad_tac display_function = function
l -> let p1, p2 = part_tac_args [] l in
(function g ->
let (p_a, p1prime, p2prime) = decompose_path (List.rev p1,p2) in
- (display_function
+ (display_function
(find_cmd (!dad_rule_list) (pf_env g)
(pf_concl g) p_a p1prime p2prime));
tclIDTAC g);;
*)
let dad_tac display_function p1 p2 g =
let (p_a, p1prime, p2prime) = decompose_path (p1,p2) in
- (display_function
+ (display_function
(find_cmd (!dad_rule_list) (pf_env g) (pf_concl g) p_a p1prime p2prime));
tclIDTAC g;;
(* Now we enter dad rule list management. *)
let add_dad_rule name patt p1 p2 depth pr command =
- dad_rule_list := (name,
+ dad_rule_list := (name,
(patt, p1, p2, depth, pr, command))::!dad_rule_list;;
let rec remove_if_exists name = function
[] -> false, []
- | ((a,b) as rule1)::tl -> if a = name then
+ | ((a,b) as rule1)::tl -> if a = name then
let result1, l = (remove_if_exists name tl) in
true, l
else
@@ -177,11 +177,11 @@ let constrain ((n : patvar),(pat : constr_pattern)) sigma =
if List.mem_assoc n sigma then
if pat = (List.assoc n sigma) then sigma
else failwith "internal"
- else
+ else
(n,pat)::sigma
-
+
(* This function is inspired from matches_core in pattern.ml *)
-let more_general_pat pat1 pat2 =
+let more_general_pat pat1 pat2 =
let rec match_rec sigma p1 p2 =
match p1, p2 with
| PMeta (Some n), m -> constrain (n,m) sigma
@@ -203,7 +203,7 @@ let more_general_pat pat1 pat2 =
| PApp (c1,arg1), PApp (c2,arg2) ->
(try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2
with Invalid_argument _ -> failwith "internal")
- | _ -> failwith "unexpected case in more_general_pat" in
+ | _ -> failwith "unexpected case in more_general_pat" in
try let _ = match_rec [] pat1 pat2 in true
with Failure "internal" -> false;;
@@ -214,7 +214,7 @@ let more_general r1 r2 =
(more_general_pat patt1 patt2) &
(is_prefix p11 p21) & (is_prefix p12 p22);;
-let not_less_general r1 r2 =
+let not_less_general r1 r2 =
not (match r1,r2 with
(_,(patt1,p11,p12,_,_,_)),
(_,(patt2,p21,p22,_,_,_)) ->
@@ -235,7 +235,7 @@ let rec add_in_list_sorting rule1 = function
rule1::this_list
and add_in_list_sorting_aux rule1 = function
[] -> []
- | b::tl ->
+ | b::tl ->
if more_general rule1 b then
b::(add_in_list_sorting rule1 tl)
else
@@ -245,7 +245,7 @@ and add_in_list_sorting_aux rule1 = function
| _ -> rule1::tl2);;
let rec sort_list = function
- [] -> []
+ [] -> []
| a::l -> add_in_list_sorting a (sort_list l);;
let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));;
diff --git a/plugins/interface/debug_tac.ml4 b/plugins/interface/debug_tac.ml4
index 79c5fe8a8e..9fade8b587 100644
--- a/plugins/interface/debug_tac.ml4
+++ b/plugins/interface/debug_tac.ml4
@@ -57,7 +57,7 @@ let no_failure = function
[Report_node(true,_,_)] -> true
| _ -> false;;
-let check_subgoals_count2
+let check_subgoals_count2
: card_holder -> int -> bool ref -> (report_holder -> tactic) -> tactic =
fun card_holder count flag t g ->
let new_report_holder = ref ([] : report_tree list) in
@@ -96,7 +96,7 @@ let count_subgoals : card_holder -> bool ref -> tactic -> tactic =
e -> card_holder := Fail;
flag := false;
tclIDTAC g;;
-
+
let count_subgoals2
: card_holder -> bool ref -> (report_holder -> tactic) -> tactic =
fun card_holder flag t g ->
@@ -139,24 +139,24 @@ let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
- In case of success of the first tactic, but count mismatch, then
Mismatch n is added to the report holder. *)
-and checked_thens: report_holder -> glob_tactic_expr -> glob_tactic_expr list -> tactic =
+and checked_thens: report_holder -> glob_tactic_expr -> glob_tactic_expr list -> tactic =
(fun report_holder t1 l g ->
let flag = ref true in
let traceable_t1 = traceable t1 in
let card_holder = ref Fail in
let new_holder = ref ([]:report_tree list) in
- let tac_t1 =
+ let tac_t1 =
if traceable_t1 then
(check_subgoals_count2 card_holder (List.length l)
flag (local_interp t1))
else
(check_subgoals_count card_holder (List.length l)
flag (Tacinterp.eval_tactic t1)) in
- let (gls, _) as result =
+ let (gls, _) as result =
tclTHEN_i tac_t1
(fun i ->
if !flag then
- (fun g ->
+ (fun g ->
let tac_i = (List.nth l i) in
if traceable tac_i then
local_interp tac_i new_holder g
@@ -174,7 +174,7 @@ and checked_thens: report_holder -> glob_tactic_expr -> glob_tactic_expr list ->
tclIDTAC) g in
let new_goal_list = sig_it gls in
(if !flag then
- report_holder :=
+ report_holder :=
(Report_node(collect_status !new_holder,
(List.length new_goal_list),
List.rev !new_holder))::!report_holder
@@ -206,7 +206,7 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti
let new_tree_holder = ref ([] : report_tree list) in
let (gls, _) as result =
tclTHEN tac_t1
- (fun (g:goal sigma) ->
+ (fun (g:goal sigma) ->
if !flag then
if traceable t2 then
local_interp t2 new_tree_holder g
@@ -273,7 +273,7 @@ let rec select_success n = function
let rec reconstruct_success_tac (tac:glob_tactic_expr) =
match tac with
TacThens (a,l) ->
- (function
+ (function
Report_node(true, n, l) -> tac
| Report_node(false, n, rl) ->
TacThens (a,List.map2 reconstruct_success_tac l rl)
@@ -292,7 +292,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
| Failed n -> TacId []
| Tree_fail r -> reconstruct_success_tac a r
| _ -> error "this error case should not happen in a THEN tactic")
- | _ ->
+ | _ ->
(function
Report_node(true, n, l) -> tac
| Failed n -> TacId []
@@ -301,7 +301,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
"this error case should not happen on an unknown tactic"
(str "error in reconstruction with " ++ fnl () ++
(pr_glob_tactic tac)));;
-
+
let rec path_to_first_error = function
| Report_node(true, _, l) ->
@@ -315,14 +315,14 @@ let rec path_to_first_error = function
let debug_tac = function
[(Tacexp ast)] ->
- (fun g ->
+ (fun g ->
let report = ref ([] : report_tree list) in
let result = local_interp ast report g in
let clean_ast = (* expand_tactic *) ast in
let report_tree =
try List.hd !report with
Failure "hd" -> (msgnl (str "report is empty"); Failed 1) in
- let success_tac =
+ let success_tac =
reconstruct_success_tac clean_ast report_tree in
let compact_success_tac = (* flatten_then *) success_tac in
msgnl (fnl () ++
@@ -339,7 +339,7 @@ add_tactic "DebugTac" debug_tac;;
Tacinterp.add_tactic "OnThen" on_then;;
-let rec clean_path tac l =
+let rec clean_path tac l =
match tac, l with
| TacThen (a,[||],b,[||]), fst::tl ->
fst::(clean_path (if fst = 1 then a else b) tl)
@@ -351,9 +351,9 @@ let rec clean_path tac l =
| _, _ -> failwith "this case should not happen in clean_path";;
let rec report_error
- : glob_tactic_expr -> goal sigma option ref -> glob_tactic_expr ref -> int list ref ->
+ : glob_tactic_expr -> goal sigma option ref -> glob_tactic_expr ref -> int list ref ->
int list -> tactic =
- fun tac the_goal the_ast returned_path path ->
+ fun tac the_goal the_ast returned_path path ->
match tac with
TacThens (a,l) ->
let the_card_holder = ref Fail in
@@ -362,12 +362,12 @@ let rec report_error
tclTHENS
(fun g ->
let result =
- check_subgoals_count
+ check_subgoals_count
the_card_holder
- (List.length l)
+ (List.length l)
the_flag
- (fun g2 ->
- try
+ (fun g2 ->
+ try
(report_error a the_goal the_ast returned_path (1::path) g2)
with
e -> (the_exn := e; raise e))
@@ -376,10 +376,10 @@ let rec report_error
result
else
(match !the_card_holder with
- Fail ->
+ Fail ->
the_ast := TacThens (!the_ast, l);
raise !the_exn
- | Goals_mismatch p ->
+ | Goals_mismatch p ->
the_ast := tac;
returned_path := path;
error ("Wrong number of tactics: expected " ^
@@ -403,7 +403,7 @@ let rec report_error
raise e))
(fun g ->
try
- let result =
+ let result =
report_error b the_goal the_ast returned_path (2::path) g in
the_count := !the_count + 1;
result
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 83c156f7bf..1a5bfaf33d 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -317,7 +317,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacLApply c -> depends_of_'constr c acc
(* Automation tactics *)
- | TacTrivial (cl, bs) ->
+ | TacTrivial (cl, bs) ->
(* TODO: Maybe make use of bs: list of hint bases to be used. *)
list_union_map depends_of_'constr cl acc
| TacAuto (_, cs, bs) ->
@@ -336,7 +336,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacClear _
| TacClearBody _
| TacMove _
- | TacRename _
+ | TacRename _
| TacRevert _ -> acc
(* Constructors *)
diff --git a/plugins/interface/history.ml b/plugins/interface/history.ml
index f73c20849a..cfd33c1861 100644
--- a/plugins/interface/history.ml
+++ b/plugins/interface/history.ml
@@ -12,7 +12,7 @@ type prf_info = {
mutable border : tree list;
prf_struct : tree};;
-let theorem_proofs = ((Hashtbl.create 17):
+let theorem_proofs = ((Hashtbl.create 17):
(string, prf_info) Hashtbl.t);;
@@ -54,12 +54,12 @@ let push_command s rank ngoals =
this_tree.sub_proofs <- new_trees
end;;
-let get_tree_for_rank thm_name rank =
- let {ranks_and_goals=l;prf_length=n} =
+let get_tree_for_rank thm_name rank =
+ let {ranks_and_goals=l;prf_length=n} =
Hashtbl.find theorem_proofs thm_name in
let rec get_tree_aux = function
[] ->
- failwith
+ failwith
"inconsistent values for thm_name and rank in get_tree_for_rank"
| (_,_,({index=i} as tree))::tl ->
if i = rank then
@@ -88,9 +88,9 @@ let parent_from_rank thm_name rank =
let first_child_command thm_name rank =
let {sub_proofs = l} = get_tree_for_rank thm_name rank in
- let rec first_child_rec = function
+ let rec first_child_rec = function
[] -> None
- | {index=i;is_open=b}::l ->
+ | {index=i;is_open=b}::l ->
if b then
(first_child_rec l)
else
@@ -104,7 +104,7 @@ let first_child_command_or_goal thm_name rank =
let {sub_proofs=l}=get_tree_for_rank thm_name rank in
match l with
[] -> None
- | ({index=i;is_open=b} as t)::_ ->
+ | ({index=i;is_open=b} as t)::_ ->
if b then
let rec get_rank n = function
[] -> failwith "A goal is lost in first_child_command_or_goal"
@@ -124,12 +124,12 @@ let next_sibling thm_name rank =
| Some real_mommy ->
let {sub_proofs=l}=real_mommy in
let rec next_sibling_aux b = function
- (opt_first, []) ->
+ (opt_first, []) ->
if b then
opt_first
else
failwith "inconsistency detected in next_sibling"
- | (opt_first, {is_open=true}::l) ->
+ | (opt_first, {is_open=true}::l) ->
next_sibling_aux b (opt_first, l)
| (Some(first),({index=i; is_open=false} as t')::l) ->
if b then
@@ -149,7 +149,7 @@ let prefix l1 l2 =
let rec remove_all_prefixes p = function
[] -> []
- | a::l ->
+ | a::l ->
if is_prefix p a then
(remove_all_prefixes p l)
else
@@ -163,8 +163,8 @@ let recompute_border tree =
else
List.fold_right recompute_border_aux l acc in
recompute_border_aux tree [];;
-
-
+
+
let historical_undo thm_name rank =
let ({ranks_and_goals=l} as proof_info)=
Hashtbl.find theorem_proofs thm_name in
@@ -180,7 +180,7 @@ let historical_undo thm_name rank =
tree.is_open <- true;
tree.sub_proofs <- [];
proof_info.border <- recompute_border proof_info.prf_struct;
- this_path_reversed::res
+ this_path_reversed::res
end
else
begin
@@ -208,7 +208,7 @@ let rec logical_undo_on_border the_tree rev_path = function
(k,tree::res)
else
(0, the_tree::tree::tl);;
-
+
let logical_undo thm_name rank =
let ({ranks_and_goals=l; border=last_border} as proof_info)=
@@ -223,7 +223,7 @@ let logical_undo thm_name rank =
let new_rank, new_offset, new_width, kept =
if is_prefix rev_ref_path this_path_rev then
(r + lex_smaller_offset), lex_smaller_offset,
- (family_width + 1 - n), false
+ (family_width + 1 - n), false
else if lex_smaller this_path_rev rev_ref_path then
r, (lex_smaller_offset - 1 + n), family_width, true
else
@@ -239,14 +239,14 @@ let logical_undo thm_name rank =
begin
tree.index <- current_rank;
ranks_undone, ((i,new_rank)::ranks_kept),
- ((new_rank, n, tree)::ranks_and_goals),
+ ((new_rank, n, tree)::ranks_and_goals),
(current_rank + 1)
end
else
((i,new_rank)::ranks_undone), ranks_kept,
ranks_and_goals, current_rank
end in
- let number_suffix, new_border =
+ let number_suffix, new_border =
logical_undo_on_border ref_tree rev_ref_path last_border in
let changed_ranks_undone, changed_ranks_kept, new_ranks_and_goals,
new_length_plus_one = logical_aux 0 number_suffix l in
@@ -265,19 +265,19 @@ let logical_undo thm_name rank =
proof_info.border <- new_border;
proof_info.ranks_and_goals <- new_ranks_and_goals;
proof_info.prf_length <- new_length_plus_one - 1;
- changed_ranks_undone, changed_ranks_kept, proof_info.prf_length,
+ changed_ranks_undone, changed_ranks_kept, proof_info.prf_length,
the_goal_index
end;;
-
+
let start_proof thm_name =
- let the_tree =
+ let the_tree =
{index=0;parent=None;path_to_root=[];is_open=true;sub_proofs=[]} in
Hashtbl.add theorem_proofs thm_name
{prf_length=0;
ranks_and_goals=[];
border=[the_tree];
prf_struct=the_tree};;
-
+
let dump_sequence chan s =
match (Hashtbl.find theorem_proofs s) with
{ranks_and_goals=l}->
@@ -294,7 +294,7 @@ let dump_sequence chan s =
output_string chan "end\n"
end;;
-
+
let proof_info_as_string s =
let res = ref "" in
match (Hashtbl.find theorem_proofs s) with
@@ -307,7 +307,7 @@ let proof_info_as_string s =
None ->
if op then
res := !res ^ "\"open goal\"\n"
- | Some {index=j} ->
+ | Some {index=j} ->
begin
res := !res ^ (string_of_int j);
res := !res ^ " -> ";
@@ -330,7 +330,7 @@ let proof_info_as_string s =
!res;;
-let dump_proof_info chan s =
+let dump_proof_info chan s =
match (Hashtbl.find theorem_proofs s) with
{prf_struct=tree} ->
let open_goal_counter = ref 0 in
@@ -341,7 +341,7 @@ let dump_proof_info chan s =
None ->
if op then
output_string chan "\"open goal\"\n"
- | Some {index=j} ->
+ | Some {index=j} ->
begin
output_string chan (string_of_int j);
output_string chan " -> ";
diff --git a/plugins/interface/line_parser.ml4 b/plugins/interface/line_parser.ml4
index 0b13a092a4..1c5afc1be7 100755
--- a/plugins/interface/line_parser.ml4
+++ b/plugins/interface/line_parser.ml4
@@ -6,7 +6,7 @@ by a precise keyword, which is also expected to appear alone on a line. *)
(* The main parsing loop procedure is "parser_loop", given at the end of this
file. It read lines one by one and checks whether they can be parsed using
a very simple parser. This very simple parser uses a lexer, which is also given
-in this file.
+in this file.
The lexical analyser:
There are only 5 sorts of tokens *)
@@ -19,7 +19,7 @@ type simple_tokens = Tspace | Tid of string | Tint of int | Tstring of string |
code in src/meta/lexer.ml of Coq revision 6.1) *)
let add_in_buff,get_buff =
let buff = ref (String.create 80) in
- (fun i x ->
+ (fun i x ->
let len = String.length !buff in
if i >= len then (buff := !buff ^ (String.create len);());
String.set !buff i x;
@@ -47,16 +47,16 @@ let get_digit c = Char.code c - code0;;
let rec parse_int intval = parser
[< ''0'..'9' as c ; i=parse_int (10 * intval + get_digit c)>] -> i
| [< >] -> Tint intval;;
-
-(* The string lexer is borrowed from the string parser of Coq V6.1
+
+(* The string lexer is borrowed from the string parser of Coq V6.1
This may be a problem if convention have changed in Coq,
However this parser is only used to recognize file names which should
not contain too many special characters *)
let rec spec_char = parser
- [< ''n' >] -> '\n'
+ [< ''n' >] -> '\n'
| [< ''t' >] -> '\t'
-| [< ''b' >] -> '\008'
+| [< ''b' >] -> '\008'
| [< ''r' >] -> '\013'
| [< ''0'..'9' as c; v= (spec1 (get_digit c)) >] ->
Char.chr v
@@ -93,7 +93,7 @@ let rec next_token = parser _count
| [< '']' >] -> Trbracket
| [< '_ ; x = next_token >] -> x;;
-(* A very simple lexical analyser to recognize a integer value behind
+(* A very simple lexical analyser to recognize a integer value behind
blank characters *)
let rec next_int = parser _count
@@ -139,7 +139,7 @@ let line_list_to_stream string_list =
count := !count + !current_length + 1;
match !reserve with
| [] -> None
- | s1::rest ->
+ | s1::rest ->
begin
buff := s1;
current_length := String.length !buff;
@@ -149,7 +149,7 @@ let line_list_to_stream string_list =
end
else
Some(String.get !buff (i - !count)));;
-
+
(* In older revisions of this file you would find a function that
does line oriented breakdown of the input channel without resorting to
@@ -196,14 +196,14 @@ let parser_loop functions input_channel =
load_syntax_action = functions in
let rec parser_loop_rec input_channel =
(let line = input_line input_channel in
- let reqid, parser_request =
- try
+ let reqid, parser_request =
+ try
(match Stream.from (token_stream (Stream.of_string line)) with
parser
| [< 'Tid "print_version" >] ->
0, PRINT_VERSION
| [< 'Tid "parse_string" ; 'Tint reqid ; 'Tlbracket ;
- 'Tid phylum ; 'Trbracket >]
+ 'Tid phylum ; 'Trbracket >]
-> reqid,PARSE_STRING phylum
| [< 'Tid "quiet_parse_string" >] ->
0,QUIET_PARSE_STRING
diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml
index f5e8be31e0..ef61a8202d 100644
--- a/plugins/interface/name_to_ast.ml
+++ b/plugins/interface/name_to_ast.ml
@@ -26,7 +26,7 @@ open Topconstr;;
of this procedure is taken from the function print_env in pretty.ml *)
let convert_env =
let convert_binder env (na, b, c) =
- match b with
+ match b with
| Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b)
| None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in
let rec cvrec env = function
@@ -34,7 +34,7 @@ let convert_env =
| b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in
cvrec (Global.env());;
-(* let mib string =
+(* let mib string =
let sp = Nametab.sp_of_id CCI (id_of_string string) in
let lobj = Lib.map_leaf (objsp_of sp) in
let (cmap, _) = outMutualInductive lobj in
@@ -52,10 +52,10 @@ let impl_args_to_string_by_pos = function
(* This function is directly inspired by implicit_args_id in pretty.ml *)
-let impl_args_to_string l =
+let impl_args_to_string l =
impl_args_to_string_by_pos (positions_of_implicits l)
-let implicit_args_id_to_ast_list id l ast_list =
+let implicit_args_id_to_ast_list id l ast_list =
(match impl_args_to_string l with
None -> ast_list
| Some(s) -> CommentString s::
@@ -67,7 +67,7 @@ let implicit_args_id_to_ast_list id l ast_list =
implicit_args_msg in pretty.ml. *)
let implicit_args_to_ast_list sp mipv =
- let implicit_args_descriptions =
+ let implicit_args_descriptions =
let ast_list = ref [] in
(Array.iteri
(fun i mip ->
@@ -78,7 +78,7 @@ let implicit_args_to_ast_list sp mipv =
(fun j idc ->
let impls = implicits_of_global
(ConstructRef ((sp,i),j+1)) in
- ast_list :=
+ ast_list :=
implicit_args_id_to_ast_list idc impls !ast_list)
mip.mind_consnames))
mipv;
@@ -86,19 +86,19 @@ let implicit_args_to_ast_list sp mipv =
match implicit_args_descriptions with
[] -> []
| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
-
+
(* This function converts constructors for an inductive definition to a
Coqast.t. It is obtained directly from print_constructors in pretty.ml *)
let convert_constructors envpar names types =
- let array_idC =
- array_map2
- (fun n t ->
+ let array_idC =
+ array_map2
+ (fun n t ->
let coercion_flag = false (* arbitrary *) in
(coercion_flag, ((dummy_loc,n), extern_constr true envpar t)))
names types in
Array.to_list array_idC;;
-
+
(* this function converts one inductive type in a possibly multiple inductive
definition *)
@@ -124,7 +124,7 @@ let mutual_to_ast_list sp mib =
VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), false, l)
:: (implicit_args_to_ast_list sp mipv);;
-let constr_to_ast v =
+let constr_to_ast v =
extern_constr true (Global.env()) v;;
let implicits_to_ast_list implicits =
@@ -137,10 +137,10 @@ let make_variable_ast name typ implicits =
((Local,Definitional),false,(*inline flag*)
[false,([dummy_loc,name], constr_to_ast typ)]))
::(implicits_to_ast_list implicits);;
-
+
let make_definition_ast name c typ implicits =
- VernacDefinition ((Global,false,Definition), (dummy_loc,name),
+ VernacDefinition ((Global,false,Definition), (dummy_loc,name),
DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
@@ -152,7 +152,7 @@ let constant_to_ast_list kn =
let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in
let l = implicits_of_global (ConstRef kn) in
(match c with
- None ->
+ None ->
make_variable_ast (id_of_label (con_label kn)) typ l
| Some c1 ->
make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
@@ -161,7 +161,7 @@ let variable_to_ast_list sp =
let (id, c, v) = Global.lookup_named sp in
let l = implicits_of_global (VarRef sp) in
(match c with
- None ->
+ None ->
make_variable_ast id v l
| Some c1 ->
make_definition_ast id c1 v l);;
@@ -180,8 +180,8 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
| "VARIABLE" -> variable_to_ast_list (basename sp)
| "CONSTANT" -> constant_to_ast_list (constant_of_kn kn)
| "INDUCTIVE" -> inductive_to_ast_list kn
- | s ->
- errorlabstrm
+ | s ->
+ errorlabstrm
"print" (str ("printing of unrecognized object " ^
s ^ " has been required"));;
@@ -191,18 +191,18 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
(* this function is inspired by print_name *)
let name_to_ast ref =
let (loc,qid) = qualid_of_reference ref in
- let l =
- try
+ let l =
+ try
match Nametab.locate qid with
| ConstRef sp -> constant_to_ast_list sp
| IndRef (sp,_) -> inductive_to_ast_list sp
| ConstructRef ((sp,_),_) -> inductive_to_ast_list sp
| VarRef sp -> variable_to_ast_list sp
- with Not_found ->
+ with Not_found ->
try (* Var locale de but, pas var de section... donc pas d'implicits *)
- let dir,name = repr_qualid qid in
+ let dir,name = repr_qualid qid in
if (repr_dirpath dir) <> [] then raise Not_found;
- let (_,c,typ) = Global.lookup_named name in
+ let (_,c,typ) = Global.lookup_named name in
(match c with
None -> make_variable_ast name typ []
| Some c1 -> make_definition_ast name c1 typ [])
diff --git a/plugins/interface/paths.ml b/plugins/interface/paths.ml
index a157ca9254..dcccc39e83 100644
--- a/plugins/interface/paths.ml
+++ b/plugins/interface/paths.ml
@@ -1,5 +1,5 @@
let int_list_to_string s l =
- List.fold_left
+ List.fold_left
(fun s -> (fun v -> s ^ " " ^ (string_of_int v)))
s
l;;
diff --git a/plugins/interface/pbp.ml b/plugins/interface/pbp.ml
index 663e4ce925..b4dfe8a769 100644
--- a/plugins/interface/pbp.ml
+++ b/plugins/interface/pbp.ml
@@ -33,8 +33,8 @@ let next_global_ident = next_global_ident_away true
let get_hyp_by_name g name =
let evd = project g in
let env = pf_env g in
- try (let judgment =
- Pretyping.Default.understand_judgment
+ try (let judgment =
+ Pretyping.Default.understand_judgment
evd env (RVar(zz, name)) in
("hyp",judgment.uj_type))
(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
@@ -132,7 +132,7 @@ let (imply_intro2: pbp_rule) = function
(f (h'::avoid) clear_names clear_flag None (kind_of_term body) path))
| _ -> None;;
-
+
(*
let (imply_intro1: pbp_rule) = function
avoid, clear_names,
@@ -140,7 +140,7 @@ let (imply_intro1: pbp_rule) = function
let h' = next_global_ident hyp_radix avoid in
let str_h' = h' in
Some(chain_tactics [make_named_intro str_h']
- (f (h'::avoid) clear_names clear_flag (Some str_h')
+ (f (h'::avoid) clear_names clear_flag (Some str_h')
(kind_of_term prem) path))
| _ -> None;;
*)
@@ -162,7 +162,7 @@ let make_pbp_atomic_tactic = function
| PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
| PbpTryAssumption (Some a) ->
TacTry (TacAtom (zz, TacExact (make_var a)))
- | PbpExists x ->
+ | PbpExists x ->
TacAtom (zz, TacSplit (false,true,[ImplicitBindings [make_pbp_pattern x]]))
| PbpGeneralize (h,args) ->
let l = List.map make_pbp_pattern args in
@@ -176,7 +176,7 @@ let make_pbp_atomic_tactic = function
let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
TacAtom
(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
- | PbpTryClear l ->
+ | PbpTryClear l ->
TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
| PbpSplit -> TacAtom (zz, TacSplit (false,false,[NoBindings]));;
@@ -188,7 +188,7 @@ let rec make_pbp_tactic = function
List.map make_pbp_tactic tl)
let (forall_elim: pbp_rule) = function
- avoid, clear_names, clear_flag,
+ avoid, clear_names, clear_flag,
Some h, Prod(Name x, _, body), 2::path, f ->
let h' = next_global_ident hyp_radix avoid in
let clear_names' = if clear_flag then h::clear_names else clear_names in
@@ -219,7 +219,7 @@ let (imply_elim2: pbp_rule) = function
Some(PbpThens
([PbpLApply h],
[chain_tactics [make_named_intro h']
- (f (h'::avoid) clear_names' false (Some h')
+ (f (h'::avoid) clear_names' false (Some h')
(kind_of_term body) path);
make_clears clear_names]))
| _ -> None;;
@@ -241,8 +241,8 @@ let notTconstr () = constant ["Logic_Type"] "notT";;
let is_matching_local a b = is_matching (pattern_of_constr a) b;;
-let rec (or_and_tree_to_intro_pattern: identifier list ->
- constr -> int list ->
+let rec (or_and_tree_to_intro_pattern: identifier list ->
+ constr -> int list ->
intro_pattern_expr * identifier list * identifier *constr
* int list * int * int) =
fun avoid c path -> match kind_of_term c, path with
@@ -251,19 +251,19 @@ fun avoid c path -> match kind_of_term c, path with
(is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
let id2 = next_global_ident hyp_radix avoid in
let cont_expr = if a = 1 then c1 else c2 in
- let cont_patt, avoid_names, id, c, path, rank, total_branches =
+ let cont_patt, avoid_names, id, c, path, rank, total_branches =
or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
- let patt_list =
+ let patt_list =
if a = 1 then
[zz,cont_patt; zz,IntroIdentifier id2]
else
[zz,IntroIdentifier id2; zz,cont_patt] in
- (IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank,
+ (IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank,
total_branches)
| (App(oper, [|c1; c2|]), 2::3::path)
when ((is_matching_local (exconstr()) oper) or
(is_matching_local (sigconstr()) oper)) ->
- (match (kind_of_term c2) with
+ (match (kind_of_term c2) with
Lambda (Name x, _, body) ->
let id1 = next_global_ident x avoid in
let cont_patt, avoid_names, id, c, path, rank, total_branches =
@@ -285,13 +285,13 @@ fun avoid c path -> match kind_of_term c, path with
[[zz,cont_patt];[zz,IntroIdentifier id2]]
else
[[zz,IntroIdentifier id2];[zz,cont_patt]] in
- (IntroOrAndPattern patt_list,
+ (IntroOrAndPattern patt_list,
avoid_names, id, c, path, new_rank, total_branches+1)
| (_, path) -> let id = next_global_ident hyp_radix avoid in
(IntroIdentifier id, (id::avoid), id, c, path, 1, 1);;
let auxiliary_goals clear_names clear_flag this_name n_aux others =
- let clear_cmd =
+ let clear_cmd =
make_clears (if clear_flag then (this_name ::clear_names) else clear_names) in
let rec clear_list = function
0 -> others
@@ -316,25 +316,25 @@ let (imply_intro3: pbp_rule) = function
(rank - 1)
((f avoid_names clear_names clear_flag (Some id)
(kind_of_term c) path)::
- auxiliary_goals clear_names clear_flag id
+ auxiliary_goals clear_names clear_flag id
(total_branches - rank) [])))
| _ -> None;;
-
+
let (and_intro: pbp_rule) = function
avoid, clear_names, clear_flag,
- None, App(and_oper, [|c1; c2|]), 2::a::path, f
+ None, App(and_oper, [|c1; c2|]), 2::a::path, f
->
if ((is_matching_local (andconstr()) and_oper) or
(is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then
let cont_term = if a = 1 then c1 else c2 in
- let cont_cmd = f avoid clear_names false None
+ let cont_cmd = f avoid clear_names false None
(kind_of_term cont_term) path in
let clear_cmd = make_clears clear_names in
let cmds =
- (if a = 1
- then [cont_cmd;clear_cmd]
+ (if a = 1
+ then [cont_cmd;clear_cmd]
else [clear_cmd;cont_cmd]) in
Some (PbpThens ([PbpSplit],cmds))
else None
@@ -342,7 +342,7 @@ let (and_intro: pbp_rule) = function
let exists_from_lambda avoid clear_names clear_flag c2 path f =
match kind_of_term c2 with
- Lambda(Name x, _, body) ->
+ Lambda(Name x, _, body) ->
Some (PbpThens ([PbpExists x],
[f avoid clear_names false None (kind_of_term body) path]))
| _ -> None;;
@@ -367,28 +367,28 @@ let (or_intro: pbp_rule) = function
avoid, clear_names, clear_flag, None,
App(or_oper, [|c1; c2 |]), 2::a::path, f ->
if ((is_matching_local (orconstr ()) or_oper) or
- (is_matching_local (sumboolconstr ()) or_oper) or
+ (is_matching_local (sumboolconstr ()) or_oper) or
(is_matching_local (sumconstr ()) or_oper))
& (a = 1 or a = 2) then
let cont_term = if a = 1 then c1 else c2 in
let fst_cmd = if a = 1 then PbpLeft else PbpRight in
- let cont_cmd = f avoid clear_names false None
+ let cont_cmd = f avoid clear_names false None
(kind_of_term cont_term) path in
Some(chain_tactics [fst_cmd] cont_cmd)
else
None
| _ -> None;;
-
+
let dummy_id = id_of_string "Dummy";;
let (not_intro: pbp_rule) = function
avoid, clear_names, clear_flag, None,
App(not_oper, [|c1|]), 2::1::path, f ->
- if(is_matching_local (notconstr ()) not_oper) or
+ if(is_matching_local (notconstr ()) not_oper) or
(is_matching_local (notTconstr ()) not_oper) then
let h' = next_global_ident hyp_radix avoid in
Some(chain_tactics [make_named_intro h']
- (f (h'::avoid) clear_names false (Some h')
+ (f (h'::avoid) clear_names false (Some h')
(kind_of_term c1) path))
else
None
@@ -407,7 +407,7 @@ let elim_with_bindings hyp_name names =
crossed.
Result is:
- a list of string indicating the names of universally quantified variables.
- - a list of integers indicating the positions of the successive
+ - a list of integers indicating the positions of the successive
universally quantified variables.
- an integer indicating the number of non-dependent products.
- the last constr object encountered during the walk down, and
@@ -421,16 +421,16 @@ let elim_with_bindings hyp_name names =
*)
-let rec down_prods: (types, constr) kind_of_term * (int list) * int ->
+let rec down_prods: (types, constr) kind_of_term * (int list) * int ->
identifier list * (int list) * int * (types, constr) kind_of_term *
- (int list) =
+ (int list) =
function
Prod(Name x, _, body), 2::path, k ->
- let res_sl, res_il, res_i, res_cstr, res_p
+ let res_sl, res_il, res_i, res_cstr, res_p
= down_prods (kind_of_term body, path, k+1) in
x::res_sl, (k::res_il), res_i, res_cstr, res_p
| Prod(Anonymous, _, body), 2::path, k ->
- let res_sl, res_il, res_i, res_cstr, res_p
+ let res_sl, res_il, res_i, res_cstr, res_p
= down_prods (kind_of_term body, path, k+1) in
res_sl, res_il, res_i+1, res_cstr, res_p
| cstr, path, _ -> [], [], 0, cstr, path;;
@@ -444,7 +444,7 @@ exception Pbp_internal of int list;;
The knowledge I have on constr structures is incomplete.
*)
-let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) =
+let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) =
function c -> function l ->
let rec delete n = function
| [] -> []
@@ -464,7 +464,7 @@ let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) =
else
result
| _ -> raise (Pbp_internal l) in
- try
+ try
(check_rec l c) = []
with Pbp_internal l -> l = [];;
@@ -475,12 +475,12 @@ let (mk_db_indices: int list -> int -> int list) =
[] -> []
| a::l -> (total - a)::(mk_db_aux l) in
mk_db_aux int_list;;
-
+
(* This proof-by-pointing rule is quite complicated, as it attempts to foresee
usages of head tactics. A first operation is to follow the path as far
as possible while staying on the spine of products (function down_prods)
- and then to check whether the next step will be an elim step. If the
+ and then to check whether the next step will be an elim step. If the
answer is true, then the built command takes advantage of the power of
head tactics. *)
@@ -497,37 +497,37 @@ let (head_tactic_patt: pbp_rule) = function
let x' = next_global_ident x avoid in
let cont_body =
Prod(Name x', c1,
- mkProd(Anonymous, body,
+ mkProd(Anonymous, body,
mkVar(dummy_id))) in
- let cont_tac
+ let cont_tac
= f avoid (h::clear_names) false None
cont_body (2::1::path) in
cont_tac::(auxiliary_goals
clear_names clear_flag
h nprems [])))
| _ -> None)
- | (str_list, _, nprems,
- App(oper,[|c1|]), 2::1::path)
+ | (str_list, _, nprems,
+ App(oper,[|c1|]), 2::1::path)
when
(is_matching_local (notconstr ()) oper) or
(is_matching_local (notTconstr ()) oper) ->
Some(chain_tactics [elim_with_bindings h str_list]
(f avoid clear_names false None (kind_of_term c1) path))
- | (str_list, _, nprems,
- App(oper, [|c1; c2|]), 2::a::path)
+ | (str_list, _, nprems,
+ App(oper, [|c1; c2|]), 2::a::path)
when ((is_matching_local (andconstr()) oper) or
(is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
let h1 = next_global_ident hyp_radix avoid in
let h2 = next_global_ident hyp_radix (h1::avoid) in
Some(PbpThens
([elim_with_bindings h str_list],
- let cont_body =
+ let cont_body =
if a = 1 then c1 else c2 in
- let cont_tac =
- f (h2::h1::avoid) (h::clear_names)
+ let cont_tac =
+ f (h2::h1::avoid) (h::clear_names)
false (Some (if 1 = a then h1 else h2))
(kind_of_term cont_body) path in
- (chain_tactics
+ (chain_tactics
[make_named_intro h1; make_named_intro h2]
cont_tac)::
(auxiliary_goals clear_names clear_flag h nprems [])))
@@ -540,9 +540,9 @@ let (head_tactic_patt: pbp_rule) = function
let x' = next_global_ident x avoid in
let cont_body =
Prod(Name x', c1,
- mkProd(Anonymous, body,
+ mkProd(Anonymous, body,
mkVar(dummy_id))) in
- let cont_tac
+ let cont_tac
= f avoid (h::clear_names) false None
cont_body (2::1::path) in
cont_tac::(auxiliary_goals
@@ -561,26 +561,26 @@ let (head_tactic_patt: pbp_rule) = function
(* h' is the name for the new intro *)
let h' = next_global_ident hyp_radix avoid in
let cont_tac =
- chain_tactics
+ chain_tactics
[make_named_intro h']
- (f
+ (f
(* h' should not be used again *)
(h'::avoid)
(* the disjunct itself can be discarded *)
(h::clear_names) false (Some h')
(kind_of_term cont_body) path) in
- let snd_tac =
+ let snd_tac =
chain_tactics
[make_named_intro h']
(make_clears (h::clear_names)) in
- let tacs1 =
+ let tacs1 =
if a = 1 then
[cont_tac; snd_tac]
else
[snd_tac; cont_tac] in
tacs1@(auxiliary_goals (h::clear_names)
false dummy_id nprems [])))
- | (str_list, int_list, nprems, c, [])
+ | (str_list, int_list, nprems, c, [])
when (check_apply c (mk_db_indices int_list nprems)) &
(match c with Prod(_,_,_) -> false
| _ -> true) &
@@ -588,7 +588,7 @@ let (head_tactic_patt: pbp_rule) = function
Some(add_clear_names_if_necessary (PbpThen [PbpApply h]) clear_names)
| _ -> None)
| _ -> None;;
-
+
let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
forall_elim; imply_intro3; imply_elim1; imply_elim2;
@@ -622,7 +622,7 @@ let default_ast optname constr path = PbpThen [PbpTryAssumption optname]
let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
let rec try_all_rules rl =
- match rl with
+ match rl with
f::tl ->
(match f (avoid, clear_names, clear_flag,
opt_name, constr, path, pbpt final_cmd) with
@@ -674,7 +674,7 @@ let rec optim3_aux str_list = function
(match cleanup_clears str_list names with
[] -> other
| l -> (PbpTryClear l)::other)
- | a::l -> a::(optim3_aux str_list l)
+ | a::l -> a::(optim3_aux str_list l)
| [] -> [];;
let rec optim3 str_list = function
@@ -694,8 +694,8 @@ let rec tactic_args_to_ints = function
| _ -> failwith "expecting only numbers";;
(*
-let pbp_tac display_function = function
- (Identifier a)::l ->
+let pbp_tac display_function = function
+ (Identifier a)::l ->
(function g ->
let str = (string_of_id a) in
let (ou,tstr) = (get_hyp_by_name g str) in
@@ -711,7 +711,7 @@ let pbp_tac display_function = function
(tactic_args_to_ints l) in
(display_function (optim exp_ast);
tclIDTAC g))
- | ((Integer n)::_) as l ->
+ | ((Integer n)::_) as l ->
(function g ->
let exp_ast =
(pbpt default_ast (pf_ids_of_hyps g) [] false
diff --git a/plugins/interface/showproof.ml b/plugins/interface/showproof.ml
index aa11609ae7..8eeeee34aa 100644
--- a/plugins/interface/showproof.ml
+++ b/plugins/interface/showproof.ml
@@ -32,7 +32,7 @@ open Genarg
(*****************************************************************************)
(*
Arbre de preuve maison:
-
+
*)
(* hypotheses *)
@@ -92,9 +92,9 @@ let tactic t =
;;
-(*
+(*
un arbre est clos s'il ne contient pas de sous-but non prouves,
-ou bien s'il a un cousin gauche qui n'est pas clos
+ou bien s'il a un cousin gauche qui n'est pas clos
ce qui fait qu'on a au plus un sous-but non clos, le premier sous-but.
*)
let update_closed nt =
@@ -117,8 +117,8 @@ let update_closed nt =
t_proof=Proof(tac,lt1)})
in update nt
;;
-
-
+
+
(*
type complet avec les hypotheses.
*)
@@ -138,7 +138,7 @@ let long_type_hyp lh t=
let seq_to_lnhyp sign sign' cl =
let lh= ref (List.map (fun (x,c,t) -> (Name x, t)) sign) in
- let nh=List.map (fun (id,c,ty) ->
+ let nh=List.map (fun (id,c,ty) ->
{hyp_name=id;
hyp_type=ty;
hyp_full_type=
@@ -156,7 +156,7 @@ let seq_to_lnhyp sign sign' cl =
let rule_is_complex r =
match r with
- Nested (Tactic
+ Nested (Tactic
((TacArg (Tacexp _)
|TacAtom (_,(TacAuto _|TacSymmetry _))),_),_) -> true
|_ -> false
@@ -219,10 +219,10 @@ let to_nproof sigma osign pf =
let rec to_nproof_rec sigma osign pf =
let {evar_hyps=sign;evar_concl=cl} = pf.goal in
let sign = Environ.named_context_of_val sign in
- let nsign = new_sign osign sign in
- let oldsign = old_sign osign sign in
+ let nsign = new_sign osign sign in
+ let oldsign = old_sign osign sign in
match pf.ref with
-
+
None -> {t_info="to_prove";
t_goal=(seq_to_lnhyp oldsign nsign cl);
t_proof=Notproved}
@@ -230,7 +230,7 @@ let to_nproof sigma osign pf =
if rule_is_complex r
then (
let p1= to_nproof_rec sigma sign (subproof_of_proof pf) in
- let ntree= fill_unproved p1
+ let ntree= fill_unproved p1
(List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
spfl) in
(match r with
@@ -253,7 +253,7 @@ let to_nproof sigma osign pf =
in update_closed (to_nproof_rec sigma osign pf)
;;
-(*
+(*
recupere l'arbre de preuve courant.
*)
@@ -262,7 +262,7 @@ let get_nproof () =
(Tacmach.proof_of_pftreestate (get_pftreestate()))
;;
-
+
(*****************************************************************************)
(*
Pprinter
@@ -273,14 +273,14 @@ let pr_void () = sphs "";;
let list_rem l = match l with [] -> [] |x::l1->l1;;
(* liste de chaines *)
-let prls l =
+let prls l =
let res = ref (sps (List.hd l)) in
- List.iter (fun s ->
+ List.iter (fun s ->
res:= sphv [ !res; spb; sps s]) (list_rem l);
!res
;;
-let prphrases f l =
+let prphrases f l =
spv (List.map (fun s -> sphv [f s; sps ","]) l)
;;
@@ -288,13 +288,13 @@ let prphrases f l =
let spi = spnb 3;;
(* en colonne *)
-let prl f l =
+let prl f l =
if l=[] then spe else spv (List.map f l);;
(*en colonne, avec indentation *)
-let prli f l =
+let prli f l =
if l=[] then spe else sph [spi; spv (List.map f l)];;
-(*
+(*
Langues.
*)
@@ -377,9 +377,9 @@ let enumerate f ln =
match ln with
[] -> []
| [x] -> [f x]
- |ln ->
- let rec enum_rec f ln =
- (match ln with
+ |ln ->
+ let rec enum_rec f ln =
+ (match ln with
[x;y] -> [f x; spb; sph [_et ();spb;f y]]
|x::l -> [sph [(f x);sps ","];spb]@(enum_rec f l)
| _ -> assert false)
@@ -506,28 +506,28 @@ let reste_a_montrer g = match !natural_language with
spb; spt g; sps ". "]
| English -> sph[ (prls ["It remains";"to";
rand ["prove";"show"]]);
- spb; spt g; sps ". "]
+ spb; spt g; sps ". "]
;;
let discutons_avec_A type_arg = match !natural_language with
French -> sphv [sps "Discutons"; spb; sps "avec"; spb;
- spt type_arg; sps ":"]
+ spt type_arg; sps ":"]
| English -> sphv [sps "Let us discuss"; spb; sps "with"; spb;
- spt type_arg; sps ":"]
+ spt type_arg; sps ":"]
;;
let utilisons_A arg1 = match !natural_language with
French -> sphv [sps (rand ["Utilisons";"Avec";"A l'aide de"]);
- spb; spt arg1; sps ":"]
+ spb; spt arg1; sps ":"]
| English -> sphv [sps (rand ["Let us use";"With";"With the help of"]);
- spb; spt arg1; sps ":"]
+ spb; spt arg1; sps ":"]
;;
let selon_les_valeurs_de_A arg1 = match !natural_language with
French -> sphv [ (prls ["Selon";"les";"valeurs";"de"]);
- spb; spt arg1; sps ":"]
+ spb; spt arg1; sps ":"]
| English -> sphv [ (prls ["According";"values";"of"]);
- spb; spt arg1; sps ":"]
+ spb; spt arg1; sps ":"]
;;
let de_A_on_a arg1 = match !natural_language with
@@ -547,9 +547,9 @@ let procedons_par_recurrence_sur_A arg1 = match !natural_language with
;;
-let calculons_la_fonction_F_de_type_T_par_recurrence_sur_son_argument_A
+let calculons_la_fonction_F_de_type_T_par_recurrence_sur_son_argument_A
nfun tfun narg = match !natural_language with
- French -> sphv [
+ French -> sphv [
sphv [ prls ["Calculons";"la";"fonction"];
spb; sps (string_of_id nfun);spb;
prls ["de";"type"];
@@ -557,7 +557,7 @@ let calculons_la_fonction_F_de_type_T_par_recurrence_sur_son_argument_A
prls ["par";"récurrence";"sur";"son";"argument"];
spb; sps (string_of_int narg); sps ":"]
]
-| English -> sphv [
+| English -> sphv [
sphv [ prls ["Let us compute";"the";"function"];
spb; sps (string_of_id nfun);spb;
prls ["of";"type"];
@@ -594,7 +594,7 @@ let coq_le_demontre_seul () = match !natural_language with
sps "Fastoche.";
sps "Trop cool"]
| English -> rand [prls ["Coq";"shows";"it"; "alone."];
- sps "Fingers in the nose."]
+ sps "Fingers in the nose."]
;;
let de_A_on_deduit_donc_B arg g = match !natural_language with
@@ -608,31 +608,31 @@ let de_A_on_deduit_donc_B arg g = match !natural_language with
let _A_est_immediat_par_B g arg = match !natural_language with
French -> sph [ spt g; spb; (prls ["est";"immédiat";"par"]);
- spb; spt arg ]
+ spb; spt arg ]
| English -> sph [ spt g; spb; (prls ["is";"immediate";"from"]);
- spb; spt arg ]
+ spb; spt arg ]
;;
let le_resultat_est arg = match !natural_language with
French -> sph [ (prls ["le";"résultat";"est"]);
- spb; spt arg ]
+ spb; spt arg ]
| English -> sph [ (prls ["the";"result";"is"]);
spb; spt arg ];;
let on_applique_la_tactique tactic tac = match !natural_language with
- French -> sphv
+ French -> sphv
[ sps "on applique";spb;sps "la tactique"; spb;tactic;spb;tac]
-| English -> sphv
+| English -> sphv
[ sps "we apply";spb;sps "the tactic"; spb;tactic;spb;tac]
;;
let de_A_il_vient_B arg g = match !natural_language with
French -> sph
- [ sps "De"; spb; spt arg; spb;
- sps "il";spb; sps "vient";spb; spt g; sps ". " ]
+ [ sps "De"; spb; spt arg; spb;
+ sps "il";spb; sps "vient";spb; spt g; sps ". " ]
| English -> sph
- [ sps "From"; spb; spt arg; spb;
- sps "it";spb; sps "comes";spb; spt g; sps ". " ]
+ [ sps "From"; spb; spt arg; spb;
+ sps "it";spb; sps "comes";spb; spt g; sps ". " ]
;;
let ce_qui_est_trivial () = match !natural_language with
@@ -690,12 +690,12 @@ type n_sort=
| Nfunction
;;
-
+
let sort_of_type t ts =
let t=(strip_outer_cast t) in
if is_Prop t
then Nprop
- else
+ else
match ts with
Prop(Null) -> Nformula
|_ -> (match (kind_of_term t) with
@@ -704,11 +704,11 @@ let sort_of_type t ts =
;;
let adrel (x,t) e =
- match x with
+ match x with
Name(xid) -> Environ.push_rel (x,None,t) e
| Anonymous -> Environ.push_rel (x,None,t) e
-let rec nsortrec vl x =
+let rec nsortrec vl x =
match (kind_of_term x) with
Prod(n,t,c)->
let vl = (adrel (n,t) vl) in nsortrec vl c
@@ -722,7 +722,7 @@ let rec nsortrec vl x =
new_sort_in_family (inductive_sort_family mip)
| Construct(c) ->
nsortrec vl (mkInd (inductive_of_constructor c))
- | Case(_,x,t,a)
+ | Case(_,x,t,a)
-> nsortrec vl x
| Cast(x,_, t)-> nsortrec vl t
| Const c -> nsortrec vl (Typeops.type_of_constant vl c)
@@ -732,7 +732,7 @@ let nsort x =
nsortrec (Global.env()) (strip_outer_cast x)
;;
-let sort_of_hyp h =
+let sort_of_hyp h =
(sort_of_type h.hyp_type (nsort h.hyp_full_type))
;;
@@ -744,14 +744,14 @@ let rec group_lhyp lh =
|[h] -> [[h]]
|h::lh ->
match group_lhyp lh with
- (h1::lh1)::lh2 ->
+ (h1::lh1)::lh2 ->
if h.hyp_type=h1.hyp_type
|| ((sort_of_hyp h)=(sort_of_hyp h1) && (sort_of_hyp h1)=Nformula)
then (h::(h1::lh1))::lh2
else [h]::((h1::lh1)::lh2)
|_-> assert false
;;
-
+
(* ln noms des hypotheses, lt leurs types *)
let natural_ghyp (sort,ln,lt) intro =
let t=List.hd lt in
@@ -761,13 +761,13 @@ let natural_ghyp (sort,ln,lt) intro =
Nprop -> soit_A_une_proposition nh ln t
| Ntype -> soit_X_un_element_de_T nh ln t
| Nfunction -> soit_F_une_fonction_de_type_T nh ln t
- | Nformula ->
+ | Nformula ->
sphv ((sps intro)::(enumerate (fun (n,t) -> tag_hypt n t)
(List.combine ln lt)))
;;
(* Cas d'une hypothese *)
-let natural_hyp h =
+let natural_hyp h =
let ns= string_of_id h.hyp_name in
let t=h.hyp_type in
let ts= (nsort h.hyp_full_type) in
@@ -782,18 +782,18 @@ let rec pr_ghyp lh intro=
Nformula -> [natural_ghyp(sort,ln,t) intro; sps ". "]
| _ -> [natural_ghyp(sort,ln,t) ""; sps ". "])
| (sort,ln,t)::lh ->
- let hp=
+ let hp=
([natural_ghyp(sort,ln,t) intro]
@(match lh with
[] -> [sps ". "]
|(sort1,ln1,t1)::lh1 ->
match sort1 with
- Nformula ->
+ Nformula ->
(let nh=List.length ln in
match sort with
- Nprop -> telle_que nh
- |Nfunction -> telle_que nh
- |Ntype -> tel_que nh
+ Nprop -> telle_que nh
+ |Nfunction -> telle_que nh
+ |Ntype -> tel_que nh
|Nformula -> [sps ". "])
| _ -> [sps ". "])) in
(sphv hp)::(pr_ghyp lh "")
@@ -860,7 +860,7 @@ let par_hypothese_de_recurrence () = match !natural_language with
let natural_lhyp lh hi =
match hi with
- All_subgoals_hyp ->
+ All_subgoals_hyp ->
( match lh with
[] -> spe
|_-> prnatural_ghyp (group_lhyp lh) (supposons ()))
@@ -896,21 +896,21 @@ let natural_lhyp lh hi =
for i=1 to nlhci do
let targ=(List.nth lhci (i-1))in
let nh=(List.nth lh (i-1)) in
- if targ="arg" || targ="argrec"
+ if targ="arg" || targ="argrec"
then
(s:=(!s)^" "^(string_of_id nh.hyp_name);
lh0:=(!lh0)@[nh])
else lh1:=(!lh1)@[nh];
done;
let introhyprec=
- (if (!lh1)=[] then spe
+ (if (!lh1)=[] then spe
else par_hypothese_de_recurrence () )
- in
+ in
if a>0 then s:="("^(!s)^")";
spv [sphv [(if ncase>1
then sph[ sps ("-"^(cas ()));spb]
else spe);
- sps !s; sps ":"];
+ sps !s; sps ":"];
prnatural_ghyp (group_lhyp !lh0) (supposons ());
introhyprec;
prl (natural_hyp) !lh1]
@@ -958,7 +958,7 @@ let rec show_goal lh ig g gs =
"intros" ->
if lh = []
then spe
- else show_goal lh "standard" g gs
+ else show_goal lh "standard" g gs
|"standard" ->
(match (sort_of_type g gs) with
Nprop -> donnons_une_proposition ()
@@ -967,7 +967,7 @@ let rec show_goal lh ig g gs =
| Nfunction ->calculons_une_fonction_de_type g)
| "apply" -> show_goal lh "" g gs
| "simpl" ->en_simplifiant_on_obtient g
- | "rewrite" -> on_obtient g
+ | "rewrite" -> on_obtient g
| "equality" -> reste_a_montrer g
| "trivial_equality" -> reste_a_montrer g
| "" -> spe
@@ -1002,14 +1002,14 @@ let first_name_hyp_of_ntree {t_goal={newhyp=lh}}=
;;
let rec find_type x t=
- match (kind_of_term (strip_outer_cast t)) with
+ match (kind_of_term (strip_outer_cast t)) with
Prod(y,ty,t) ->
(match y with
- Name y ->
+ Name y ->
if x=(string_of_id y) then ty
else find_type x t
| _ -> find_type x t)
- |_-> assert false
+ |_-> assert false
;;
(***********************************************************************
@@ -1061,7 +1061,7 @@ let is_equality_tac = function
let equalities_ntree ig ntree =
let rec equalities_ntree ig ntree =
- if not (is_equality (concl ntree))
+ if not (is_equality (concl ntree))
then []
else
match (proof ntree) with
@@ -1075,8 +1075,8 @@ let equalities_ntree ig ntree =
then res
else (ig,ntree)::res)
else [(ig,ntree)]
- in
- equalities_ntree ig ntree
+ in
+ equalities_ntree ig ntree
;;
let remove_seq_of_terms l =
@@ -1091,7 +1091,7 @@ let remove_seq_of_terms l =
let list_to_eq l o=
let switch = fun h h' -> (if o then h else h') in
match l with
- [a] -> spt (fst a)
+ [a] -> spt (fst a)
| (a,h)::(b,h')::l ->
let rec list_to_eq h l =
match l with
@@ -1100,7 +1100,7 @@ let list_to_eq l o=
(sph [sps "="; spb; spt b; spb;tag_uselemma (switch h h') spe])
:: (list_to_eq (switch h' h) l)
in sph [spt a; spb;
- spv ((sph [sps "="; spb; spt b; spb;
+ spv ((sph [sps "="; spb; spt b; spb;
tag_uselemma (switch h h') spe])
::(list_to_eq (switch h' h) l))]
| _ -> assert false
@@ -1131,7 +1131,7 @@ let rec natural_ntree ig ntree =
[] ->spe
| [_] -> spe
| _::l -> sphv[sps ": ";
- prli (natural_ntree
+ prli (natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="standard"})
l])])
@@ -1157,7 +1157,7 @@ let rec natural_ntree ig ntree =
spv [(natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g (nsort gf) "");
sph !ltext;
-
+
natural_ntree {ihsg=All_subgoals_hyp;
isgintro=
let (t1,t2)= terms_of_equality (concl ntree) in
@@ -1171,13 +1171,13 @@ let rec natural_ntree ig ntree =
let gs=nsort gf in
match p with
Notproved -> spv [ (natural_lhyp lh ig.ihsg);
- sph [spi; sps (intro_not_proved_goal gs); spb;
+ sph [spi; sps (intro_not_proved_goal gs); spb;
tag_toprove g ]
]
| Proof (TacId _,ltree) -> natural_ntree ig (List.hd ltree)
- | Proof (TacAtom (_,tac),ltree) ->
- (let ntext =
+ | Proof (TacAtom (_,tac),ltree) ->
+ (let ntext =
match tac with
(* Pas besoin de l'argument éventuel de la tactique *)
TacIntroPattern _ -> natural_intros ig lh g gs ltree
@@ -1197,9 +1197,9 @@ let rec natural_ntree ig ntree =
| TacAssumption -> natural_trivial ig lh g gs ltree
| TacClear _ -> natural_clear ig lh g gs ltree
(* Besoin de l'argument de la tactique *)
- | TacSimpleInductionDestruct (true,NamedHyp id) ->
+ | TacSimpleInductionDestruct (true,NamedHyp id) ->
natural_induction ig lh g gs ge id ltree false
- | TacExtend (_,"InductionIntro",[a]) ->
+ | TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
natural_induction ig lh g gs ge id ltree true
| TacApply (_,false,[c,_],None) ->
@@ -1232,7 +1232,7 @@ let rec natural_ntree ig ntree =
ntext (* spwithtac ntext tactic*)
)
| Proof _ -> failwith "Don't know what to do with that"
- in
+ in
if info<>"not_proved"
then spshrink info ntext
else ntext
@@ -1241,7 +1241,7 @@ and natural_generic ig lh g gs tactic tac ltree =
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
on_applique_la_tactique tactic tac ;
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="standard"})
ltree)
@@ -1258,7 +1258,7 @@ and natural_intros ig lh g gs ltree =
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
- (prl (natural_ntree
+ (prl (natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="intros"})
ltree)
@@ -1269,7 +1269,7 @@ and natural_apply ig lh g gs arg ltree =
[] ->
spv
[ (natural_lhyp lh ig.ihsg);
- de_A_il_vient_B arg g
+ de_A_il_vient_B arg g
]
| [sg]->
spv
@@ -1280,10 +1280,10 @@ and natural_apply ig lh g gs arg ltree =
else ""}
g gs "");
grace_a_A_il_suffit_de_montrer_LA arg [spt sg];
- sph [spi ; natural_ntree
+ sph [spi ; natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="apply"} (List.hd ltree)]
- ]
+ ]
| _ ->
let ln = List.map (fun _ -> new_name()) lg in
spv
@@ -1298,7 +1298,7 @@ and natural_apply ig lh g gs arg ltree =
lg ln);
sph [spi; spv (List.map2
(fun x n -> sph [sps ("("^n^"):"); spb;
- natural_ntree
+ natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="apply"} x])
ltree ln)]
@@ -1310,26 +1310,26 @@ and natural_rem_goals ltree =
| [sg]->
spv
[ reste_a_montrer_LA [spt sg];
- sph [spi ; natural_ntree
+ sph [spi ; natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="apply"} (List.hd ltree)]
- ]
+ ]
| _ ->
let ln = List.map (fun _ -> new_name()) lg in
spv
- [ reste_a_montrer_LA
+ [ reste_a_montrer_LA
(List.map2 (fun g n -> sph [sps ("("^n^")"); spb; spt g])
lg ln);
sph [spi; spv (List.map2
(fun x n -> sph [sps ("("^n^"):"); spb;
- natural_ntree
+ natural_ntree
{ihsg=All_subgoals_hyp;
isgintro="apply"} x])
ltree ln)]
]
and natural_exact ig lh g gs arg ltree =
spv
- [
+ [
(natural_lhyp lh ig.ihsg);
(let {ihsg=pi;isgintro=ig}= ig in
(show_goal2 lh {ihsg=pi;isgintro=""}
@@ -1343,7 +1343,7 @@ and natural_cut ig lh g gs arg ltree =
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro="standard"})
(List.rev ltree));
de_A_on_deduit_donc_B arg g
@@ -1353,18 +1353,18 @@ and natural_cutintro ig lh g gs arg ltree =
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
sph [spi;
- (natural_ntree
+ (natural_ntree
{ihsg=All_subgoals_hyp;isgintro=""}
(List.nth ltree 1))];
sph [spi;
- (natural_ntree
+ (natural_ntree
{ihsg=No_subgoals_hyp;isgintro=""}
(List.nth ltree 0))]
]
and whd_betadeltaiota x = whd_betaiota Evd.empty x
and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
and prod_head t =
- match (kind_of_term (strip_outer_cast t)) with
+ match (kind_of_term (strip_outer_cast t)) with
Prod(_,_,c) -> prod_head c
(* |App(f,a) -> f *)
| _ -> t
@@ -1386,7 +1386,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
let type_arg= targ1 (* List.nth targ (mis_index dmi)*) in
if ncti<>1
(* Zéro ou Plusieurs constructeurs *)
- then (
+ then (
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1404,7 +1404,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
then (arity_of_constr_of_mind env indf !ci)
else 0 in
let ici= (!ci) in
- sph[ (natural_ntree
+ sph[ (natural_ntree
{ihsg=
(match (nsort targ1) with
Prop(Null) ->
@@ -1420,7 +1420,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
(nhd ltree ((List.length ltree)- ncti)))])
] )
(* Cas d'un seul constructeur *)
- else (
+ else (
spv
[ (natural_lhyp lh ig.ihsg);
@@ -1433,7 +1433,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
then (arity_of_constr_of_mind env indf 1)
else 0 in
let _ici= 1 in
- sph[ (natural_ntree
+ sph[ (natural_ntree
{ihsg=
(match (nsort targ1) with
Prop(Null) ->
@@ -1446,7 +1446,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
]);
(sph [spi; (natural_rem_goals
(nhd ltree ((List.length ltree)- 1)))])
- ]
+ ]
)
(* with _ ->natural_generic ig lh g gs (sps "Case") (spt arg1) ltree *)
@@ -1455,7 +1455,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
Elim
*)
and prod_list_var t =
- match (kind_of_term (strip_outer_cast t)) with
+ match (kind_of_term (strip_outer_cast t)) with
Prod(_,t,c) -> t::(prod_list_var c)
|_ -> []
and hd_is_mind t ti =
@@ -1486,7 +1486,7 @@ and mind_ind_info_hyp_constr indf c =
!lr
(*
mind_ind_info_hyp_constr "le" 2;;
-donne ["arg"; "argrec"]
+donne ["arg"; "argrec"]
mind_ind_info_hyp_constr "le" 1;;
donne []
mind_ind_info_hyp_constr "nat" 2;;
@@ -1518,7 +1518,7 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
then mind_ind_info_hyp_constr indf !ci
else [] in
let ici= (!ci) in
- sph[ (natural_ntree
+ sph[ (natural_ntree
{ihsg=
(match (nsort targ1) with
Prop(Null) ->
@@ -1538,7 +1538,7 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
(*****************************************************************************)
(*
InductionIntro n
-*)
+*)
and natural_induction ig lh g gs ge arg2 ltree with_intros=
let env = (gLOB (g_env (List.hd ltree))) in
let arg1= mkVar arg2 in
@@ -1572,12 +1572,12 @@ and natural_induction ig lh g gs ge arg2 ltree with_intros=
(fun treearg -> ci:=!ci+1;
let nci=(constr_of_mind mip !ci) in
let aci=(arity_of_constr_of_mind env indf !ci) in
- let hci=
+ let hci=
if with_intros
then mind_ind_info_hyp_constr indf !ci
else [] in
let ici= (!ci) in
- sph[ (natural_ntree
+ sph[ (natural_ntree
{ihsg=
(match (nsort targ1) with
Prop(Null) ->
@@ -1606,47 +1606,47 @@ and natural_fix ig lh g gs narg ltree =
spv
[ (natural_lhyp lh ig.ihsg);
calculons_la_fonction_F_de_type_T_par_recurrence_sur_son_argument_A nfun tfun narg;
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro=""})
ltree)
]
| _ -> assert false
and natural_reduce ig lh g gs ge mode la ltree =
match la with
- {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr ->
+ {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr ->
spv
[ (natural_lhyp lh ig.ihsg);
- (show_goal2 lh ig g gs "");
- (prl (natural_ntree
+ (show_goal2 lh ig g gs "");
+ (prl (natural_ntree
{ihsg=All_subgoals_hyp;isgintro="simpl"})
ltree)
]
| {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr ->
spv
[ (natural_lhyp lh ig.ihsg);
- (show_goal2 lh ig g gs "");
- (prl (natural_ntree
+ (show_goal2 lh ig g gs "");
+ (prl (natural_ntree
{ihsg=Reduce_hyp;isgintro=""})
ltree)
]
| _ -> assert false
and natural_split ig lh g gs ge la ltree =
match la with
- [arg] ->
+ [arg] ->
let _env= (gLOB ge) in
let arg1= (*dbize _env*) arg in
spv
[ (natural_lhyp lh ig.ihsg);
- (show_goal2 lh ig g gs "");
+ (show_goal2 lh ig g gs "");
pour_montrer_G_la_valeur_recherchee_est_A g arg1;
- (prl (natural_ntree
+ (prl (natural_ntree
{ihsg=All_subgoals_hyp;isgintro="standard"})
ltree)
]
| [] ->
spv
[ (natural_lhyp lh ig.ihsg);
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro="standard"})
ltree)
]
@@ -1660,9 +1660,9 @@ and natural_generalize ig lh g gs ge la ltree =
(* let type_arg=type_of_ast ge arg in*)
spv
[ (natural_lhyp lh ig.ihsg);
- (show_goal2 lh ig g gs "");
+ (show_goal2 lh ig g gs "");
on_se_sert_de_A arg1;
- (prl (natural_ntree
+ (prl (natural_ntree
{ihsg=All_subgoals_hyp;isgintro=""})
ltree)
]
@@ -1670,23 +1670,23 @@ and natural_generalize ig lh g gs ge la ltree =
and natural_right ig lh g gs ltree =
spv
[ (natural_lhyp lh ig.ihsg);
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro="standard"})
- ltree);
- d_ou_A g
+ ltree);
+ d_ou_A g
]
and natural_left ig lh g gs ltree =
spv
[ (natural_lhyp lh ig.ihsg);
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro="standard"})
- ltree);
- d_ou_A g
+ ltree);
+ d_ou_A g
]
and natural_auto ig lh g gs ltree =
match ig.isgintro with
"trivial_equality" -> spe
- | _ ->
+ | _ ->
if ltree=[]
then sphv [(natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1717,7 +1717,7 @@ and natural_trivial ig lh g gs ltree =
ce_qui_est_trivial () ]
else spv [(natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs ". ");
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro="standard"})
ltree)]
and natural_rewrite ig lh g gs arg ltree =
@@ -1725,7 +1725,7 @@ and natural_rewrite ig lh g gs arg ltree =
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
en_utilisant_l_egalite_A arg;
- (prli(natural_ntree
+ (prli(natural_ntree
{ihsg=All_subgoals_hyp;isgintro="rewrite"})
ltree)
]
@@ -1768,18 +1768,18 @@ CAMLLIB=/usr/local/lib/ocaml
CAMLP4LIB=/usr/local/lib/camlp4
export CAMLLIB
export COQTOP
-export CAMLP4LIB
+export CAMLP4LIB
cd d:/Tools/pcoq/src/text
d:/Tools/coq-7avril/bin/coqtop.byte.exe -I /cygdrive/D/Tools/pcoq/src/abs_syntax -I /cygdrive/D/Tools/pcoq/src/text -I /cygdrive/D/Tools/pcoq/src/coq -I /cygdrive/D/Tools/pcoq/src/pbp -I /cygdrive/D/Tools/pcoq/src/dad -I /cygdrive/D/Tools/pcoq/src/history
-
-
+
+
Lemma l1: (A, B : Prop) A \/ B -> B -> A.
Intros.
Elim H.
Auto.
Qed.
-
+
Drop.
@@ -1806,7 +1806,7 @@ Pp_control.set_depth_boxes 100;;
#install_printer pproof;;
ep();;
-let bidon = ref (constr_of_string "O");;
+let bidon = ref (constr_of_string "O");;
#trace to_nproof;;
***********************************************************************)
diff --git a/plugins/interface/showproof_ct.ml b/plugins/interface/showproof_ct.ml
index dd7f455d79..7632ebdfb5 100644
--- a/plugins/interface/showproof_ct.ml
+++ b/plugins/interface/showproof_ct.ml
@@ -26,20 +26,20 @@ let spe = sphs "";;
let spb = sps " ";;
let spr = sps "Retour chariot pour Show proof";;
-let spnb n =
+let spnb n =
let s = ref "" in
for i=1 to n do s:=(!s)^" "; done; sps !s
;;
let rec spclean l =
- match l with
+ match l with
[] -> []
|x::l -> if x=spe then (spclean l) else x::(spclean l)
;;
-let spnb n =
+let spnb n =
let s = ref "" in
for i=1 to n do s:=(!s)^" "; done; sps !s
;;
@@ -62,13 +62,13 @@ let root_of_text_proof t=
CT_text_op [ct_text "root_of_text_proof";
t]
;;
-
+
let spshrink info t =
CT_text_op [ct_text "shrink";
CT_text_op [ct_text info;
t]]
;;
-
+
let spuselemma intro x y =
CT_text_op [ct_text "uselemma";
ct_text intro;
@@ -105,7 +105,7 @@ let spv l =
let l= spclean l in
CT_text_v l
;;
-
+
let sph l =
let l= spclean l in
CT_text_h l
@@ -118,12 +118,12 @@ let sphv l =
;;
let rec prlist_with_sep f g l =
- match l with
+ match l with
[] -> hov 0 (mt ())
|x::l1 -> hov 0 ((g x) ++ (f ()) ++ (prlist_with_sep f g l1))
;;
-
-let rec sp_print x =
+
+let rec sp_print x =
match x with
| CT_coerce_ID_to_TEXT (CT_ident s)
-> (match s with
@@ -162,7 +162,7 @@ let rec sp_print x =
(CT_coerce_INT_to_SIGNED_INT
(CT_int x)) -> x
| _ -> raise (Failure "sp_print")) p) in
- h 0 (sp_print g ++ spc () ++ str "<i>(" ++ str hyp ++ str ")</i>")
+ h 0 (sp_print g ++ spc () ++ str "<i>(" ++ str hyp ++ str ")</i>")
| CT_text_h l ->
h 0 (prlist_with_sep (fun () -> mt ())
@@ -178,7 +178,7 @@ let rec sp_print x =
h 0 (str ("("^info^": ") ++ sp_print t ++ str ")")
| CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "root_of_text_proof");
t]->
- sp_print t
+ sp_print t
| _ -> str "..."
;;
-
+
diff --git a/plugins/interface/translate.ml b/plugins/interface/translate.ml
index 559860b2fc..48f35ebab2 100644
--- a/plugins/interface/translate.ml
+++ b/plugins/interface/translate.ml
@@ -25,9 +25,9 @@ let translate_constr at_top env c =
(*translates a named_context into a centaur-tree --> PREMISES_LIST *)
(* this code is inspired from printer.ml (function pr_named_context_of) *)
let translate_sign env =
- let l =
+ let l =
Environ.fold_named_context
- (fun env (id,v,c) l ->
+ (fun env (id,v,c) l ->
(match v with
None ->
CT_premise(CT_ident(string_of_id id), translate_constr false env c)
@@ -36,19 +36,19 @@ let translate_sign env =
(CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)),
translate_constr false env v1,
translate_constr false env c))::l)
- env ~init:[]
+ env ~init:[]
in
CT_premises_list l;;
-
+
(* the function rev_and_compact performs two operations:
1- it reverses the list of integers given as argument
2- it replaces sequences of "1" by a negative number that is
the length of the sequence. *)
let rec rev_and_compact l = function
[] -> l
- | 1::tl ->
+ | 1::tl ->
(match l with
- n::tl' ->
+ n::tl' ->
if n < 0 then
rev_and_compact ((n - 1)::tl') tl
else
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index be7472a486..a322c7a72b 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -17,7 +17,7 @@ open Goptions;;
(* // Verify whether this is dead code, as of coq version 7 *)
-(* The following three sentences have been added to cope with a change
+(* The following three sentences have been added to cope with a change
of strategy from the Coq team in the way rules construct ast's. The
problem is that now grammar rules will refer to identifiers by giving
their absolute name, using the mutconstruct when needed. Unfortunately,
@@ -80,7 +80,7 @@ let ctv_FORMULA_OPT_NONE =
let ctv_PATTERN_OPT_NONE = CT_coerce_NONE_to_PATTERN_OPT CT_none;;
-let ctv_DEF_BODY_OPT_NONE = CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT
+let ctv_DEF_BODY_OPT_NONE = CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT
ctv_FORMULA_OPT_NONE;;
let ctf_ID_OPT_OR_ALL_SOME s =
@@ -202,7 +202,7 @@ let apply_or_by_notation f = function
| AN x -> f x
| ByNotation _ -> xlate_error "TODO: ByNotation"
-let tac_qualid_to_ct_ID ref =
+let tac_qualid_to_ct_ID ref =
CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
let loc_qualid_to_ct_ID ref =
@@ -229,10 +229,10 @@ let xlate_class = function
let id_to_pattern_var ctid =
match ctid with
| CT_metaid _ -> xlate_error "metaid not expected in pattern_var"
- | CT_ident "_" ->
+ | CT_ident "_" ->
CT_coerce_ID_OPT_to_MATCH_PATTERN (CT_coerce_NONE_to_ID_OPT CT_none)
| CT_ident id_string ->
- CT_coerce_ID_OPT_to_MATCH_PATTERN
+ CT_coerce_ID_OPT_to_MATCH_PATTERN
(CT_coerce_ID_to_ID_OPT (CT_ident id_string))
| CT_metac _ -> assert false;;
@@ -250,7 +250,7 @@ let xlate_qualid a =
let d,i = Libnames.repr_qualid a in
let l = Names.repr_dirpath d in
List.fold_left (fun s i1 -> (string_of_id i1) ^ "." ^ s) (string_of_id i) l;;
-
+
(* // The next two functions should be modified to make direct reference
to a notation operator *)
let notation_to_formula s l = CT_notation(CT_string s, CT_formula_list l);;
@@ -267,19 +267,19 @@ let rec xlate_match_pattern =
CT_pattern_app
(id_to_pattern_var (xlate_reference f1),
CT_match_pattern_ne_list
- (xlate_match_pattern arg1,
+ (xlate_match_pattern arg1,
List.map xlate_match_pattern args))
| CPatAlias (_, pattern, id) ->
CT_pattern_as
(xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
| CPatOr (_,l) -> xlate_error "CPatOr: TODO"
- | CPatDelimiters(_, key, p) ->
+ | CPatDelimiters(_, key, p) ->
CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
| CPatPrim (_,Numeral n) ->
CT_coerce_NUM_to_MATCH_PATTERN
(CT_int_encapsulator(Bigint.to_string n))
| CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
- | CPatNotation(_, s, (l,[])) ->
+ | CPatNotation(_, s, (l,[])) ->
CT_pattern_notation(CT_string s,
CT_match_pattern_list(List.map xlate_match_pattern l))
| CPatNotation(_, s, (l,_)) ->
@@ -331,26 +331,26 @@ and xlate_binder_l = function
LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
| LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n,
xlate_formula v))
-and
+and
xlate_match_pattern_ne_list = function
[] -> assert false
- | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a,
+ | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a,
List.map xlate_match_pattern l)
and translate_one_equation = function
(_,[_,lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
| _ -> xlate_error "TODO: disjunctive multiple patterns"
-and
+and
xlate_binder_ne_list = function
[] -> assert false
| a::l -> CT_binder_ne_list(xlate_binder a, List.map xlate_binder l)
-and
+and
xlate_binder_list = function
l -> CT_binder_list( List.map xlate_binder_l l)
and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
CRef r -> varc (xlate_reference r)
| CArrow(_,a,b)-> CT_arrowc (xlate_formula a, xlate_formula b)
- | CProdN(_,ll,b) as whole_term ->
+ | CProdN(_,ll,b) as whole_term ->
let rec gather_binders = function
CProdN(_, ll, b) ->
ll@(gather_binders b)
@@ -358,27 +358,27 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
let rec fetch_ultimate_body = function
CProdN(_, _, b) -> fetch_ultimate_body b
| a -> a in
- CT_prodc(xlate_binder_ne_list (gather_binders whole_term),
+ CT_prodc(xlate_binder_ne_list (gather_binders whole_term),
xlate_formula (fetch_ultimate_body b))
| CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
- | CLetIn(_, v, a, b) ->
+ | CLetIn(_, v, a, b) ->
CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
- | CAppExpl(_, (Some n, r), l) ->
+ | CAppExpl(_, (Some n, r), l) ->
let l', last = decompose_last l in
CT_proj(xlate_formula last,
CT_formula_ne_list
(CT_bang(varc (xlate_reference r)),
List.map xlate_formula l'))
| CAppExpl(_, (None, r), []) -> CT_bang(varc(xlate_reference r))
- | CAppExpl(_, (None, r), l) ->
+ | CAppExpl(_, (None, r), l) ->
CT_appc(CT_bang(varc (xlate_reference r)),
xlate_formula_ne_list l)
- | CApp(_, (Some n,f), l) ->
+ | CApp(_, (Some n,f), l) ->
let l', last = decompose_last l in
- CT_proj(xlate_formula_expl last,
+ CT_proj(xlate_formula_expl last,
CT_formula_ne_list
(xlate_formula f, List.map xlate_formula_expl l'))
- | CApp(_, (_,f), l) ->
+ | CApp(_, (_,f), l) ->
CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
| CRecord (_,_,_) -> xlate_error "CRecord: TODO"
| CCases (_, _, _, [], _) -> assert false
@@ -387,14 +387,14 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
List.map xlate_matched_formula tml),
xlate_formula_opt ret_type,
CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
- | CLetTuple (_,a::l, ret_info, c, b) ->
+ | CLetTuple (_,a::l, ret_info, c, b) ->
CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
List.map xlate_id_opt_aux l),
xlate_return_info ret_info,
xlate_formula c,
xlate_formula b)
| CLetTuple (_, [], _, _, _) -> xlate_error "NOT parsed: Let with ()"
- | CIf (_,c, ret_info, b1, b2) ->
+ | CIf (_,c, ret_info, b1, b2) ->
CT_if
(xlate_formula c, xlate_return_info ret_info,
xlate_formula b1, xlate_formula b2)
@@ -403,16 +403,16 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CNotation(_, s,(l,[])) -> notation_to_formula s (List.map xlate_formula l)
| CNotation(_, s,(l,_)) -> xlate_error "CNotation (recursive): TODO"
| CGeneralization(_,_,_,_) -> xlate_error "CGeneralization: TODO"
- | CPrim (_, Numeral i) ->
+ | CPrim (_, Numeral i) ->
CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
| CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
- | CHole _ -> CT_existvarc
+ | CHole _ -> CT_existvarc
(* I assume CDynamic has been inserted to make free form extension of
the language possible, but this would go against the logic of pcoq anyway. *)
| CDynamic (_, _) -> assert false
- | CDelimiters (_, key, num) ->
+ | CDelimiters (_, key, num) ->
CT_num_encapsulator(CT_num_type key , xlate_formula num)
- | CCast (_, e, CastConv (_, t)) ->
+ | CCast (_, e, CastConv (_, t)) ->
CT_coerce_TYPED_FORMULA_to_FORMULA
(CT_typed_formula(xlate_formula e, xlate_formula t))
| CCast (_, e, CastCoerce) -> assert false
@@ -423,13 +423,13 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CPatVar (_, (true, s)) ->
xlate_error "Second order variable not supported"
| CEvar _ -> xlate_error "CEvar not supported"
- | CCoFix (_, (_, id), lm::lmi) ->
+ | CCoFix (_, (_, id), lm::lmi) ->
let strip_mutcorec ((_, fid), bl,arf, ardef) =
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
xlate_formula arf, xlate_formula ardef) in
CT_cofixc(xlate_ident id,
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
- | CFix (_, (_, id), lm::lmi) ->
+ | CFix (_, (_, id), lm::lmi) ->
let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) =
let struct_arg = make_fix_struct (n, bl) in
let arf = xlate_formula arf in
@@ -439,12 +439,12 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
struct_arg, arf, ardef)
| _ -> xlate_error "mutual recursive" in
- CT_fixc (xlate_ident id,
+ CT_fixc (xlate_ident id,
CT_fix_binder_list
- (CT_coerce_FIX_REC_to_FIX_BINDER
- (strip_mutrec lm), List.map
+ (CT_coerce_FIX_REC_to_FIX_BINDER
+ (strip_mutrec lm), List.map
(fun x-> CT_coerce_FIX_REC_to_FIX_BINDER (strip_mutrec x))
- lmi))
+ lmi))
| CCoFix _ -> assert false
| CFix _ -> assert false
and xlate_matched_formula = function
@@ -454,18 +454,18 @@ and xlate_matched_formula = function
CT_formula_in(xlate_formula f, xlate_formula y)
| (f, (Some x, None)) ->
CT_formula_as(xlate_formula f, xlate_id_opt_aux x)
- | (f, (None, None)) ->
+ | (f, (None, None)) ->
CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f)
and xlate_formula_expl = function
(a, None) -> xlate_formula a
- | (a, Some (_,ExplByPos (i, _))) ->
+ | (a, Some (_,ExplByPos (i, _))) ->
xlate_error "explicitation of implicit by rank not supported"
| (a, Some (_,ExplByName i)) ->
CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
and xlate_formula_expl_ne_list = function
[] -> assert false
| a::l -> CT_formula_ne_list(xlate_formula_expl a, List.map xlate_formula_expl l)
-and xlate_formula_ne_list = function
+and xlate_formula_ne_list = function
[] -> assert false
| a::l -> CT_formula_ne_list(xlate_formula a, List.map xlate_formula l);;
@@ -489,17 +489,17 @@ let xlate_hyp_location =
| (occs, AI (_,id)), InHypValueOnly ->
CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
| (occs, AI (_,id)), InHyp when occs = all_occurrences_expr ->
- CT_coerce_UNFOLD_to_HYP_LOCATION
+ CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_coerce_ID_to_UNFOLD (xlate_ident id))
| ((_,a::l as occs), AI (_,id)), InHyp ->
let nums = nums_of_occs occs in
let a = List.hd nums and l = List.tl nums in
- CT_coerce_UNFOLD_to_HYP_LOCATION
- (CT_unfold_occ (xlate_ident id,
- CT_int_ne_list(num_or_var_to_int a,
+ CT_coerce_UNFOLD_to_HYP_LOCATION
+ (CT_unfold_occ (xlate_ident id,
+ CT_int_ne_list(num_or_var_to_int a,
nums_or_var_to_int_list_aux l)))
| (_, AI (_,id)), InHyp -> xlate_error "Unused" (* (true,]) *)
- | (_, MetaId _),_ ->
+ | (_, MetaId _),_ ->
xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
@@ -510,8 +510,8 @@ let xlate_clause cls =
None -> CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR CT_star
| Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
CT_clause
- (hyps_info,
- if cls.concl_occs <> no_occurrences_expr then
+ (hyps_info,
+ if cls.concl_occs <> no_occurrences_expr then
CT_coerce_STAR_to_STAR_OPT CT_star
else
CT_coerce_NONE_to_STAR_OPT CT_none)
@@ -577,7 +577,7 @@ let xlate_quantified_hypothesis = function
| NamedHyp id -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id)
let xlate_quantified_hypothesis_opt = function
- | None ->
+ | None ->
CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE
| Some (AnonHyp n) -> xlate_int_to_id_or_int_opt n
| Some (NamedHyp id) -> xlate_id_to_id_or_int_opt id;;
@@ -586,7 +586,7 @@ let xlate_id_or_int = function
ArgArg n -> CT_coerce_INT_to_ID_OR_INT(CT_int n)
| ArgVar(_, s) -> CT_coerce_ID_to_ID_OR_INT(xlate_ident s);;
-let xlate_explicit_binding (loc,h,c) =
+let xlate_explicit_binding (loc,h,c) =
CT_binding (xlate_quantified_hypothesis h, xlate_formula c)
let xlate_bindings = function
@@ -630,7 +630,7 @@ let rec xlate_intro_pattern (loc,pat) = match pat with
| IntroOrAndPattern (fp::ll) ->
CT_disj_pattern
(CT_intro_patt_list(List.map xlate_intro_pattern fp),
- List.map
+ List.map
(fun l ->
CT_intro_patt_list(List.map xlate_intro_pattern l))
ll)
@@ -651,7 +651,7 @@ let is_tactic_special_case = function
| _ -> false;;
let xlate_context_pattern = function
- | Term v ->
+ | Term v ->
CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
| Subterm (b, idopt, v) -> (* TODO: application pattern *)
CT_context(xlate_ident_opt idopt, xlate_formula v)
@@ -677,7 +677,7 @@ let xlate_int_or_constr = function
| ElimOnIdent(_,i) ->
CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
(CT_coerce_ID_to_ID_OR_INT(xlate_ident i))
- | ElimOnAnonHyp i ->
+ | ElimOnAnonHyp i ->
CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
(CT_coerce_INT_to_ID_OR_INT(CT_int i));;
@@ -686,11 +686,11 @@ let xlate_using = function
| Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
let xlate_one_unfold_block = function
- ((true,[]),qid) ->
+ ((true,[]),qid) ->
CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid)
| (((_,_::_) as occs), qid) ->
let l = nums_of_occs occs in
- CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid,
+ CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid,
nums_or_var_to_int_ne_list (List.hd l) (List.tl l))
| ((false,[]), qid) -> xlate_error "Unused"
;;
@@ -705,7 +705,7 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
function
| TacVoid ->
CT_void
- | Tacexp t ->
+ | Tacexp t ->
CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_tactic t)
| Integer n ->
CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG
@@ -724,7 +724,7 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
CT_coerce_EVAL_CMD_to_TACTIC_ARG
(CT_eval(CT_coerce_NONE_to_INT_OPT CT_none, xlate_red_tactic r,
xlate_formula c))
- | ConstrMayEval(ConstrTypeOf(c)) ->
+ | ConstrMayEval(ConstrTypeOf(c)) ->
CT_coerce_TERM_CHANGE_to_TACTIC_ARG(CT_check_term(xlate_formula c))
| MetaIdArg _ ->
xlate_error "MetaIdArg should only be used in quotations"
@@ -753,9 +753,9 @@ and xlate_red_tactic =
| CbvVm -> CT_cbvvm
| Hnf -> CT_hnf
| Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
- | Simpl (Some (occs,c)) ->
+ | Simpl (Some (occs,c)) ->
let l = nums_of_occs occs in
- CT_simpl
+ CT_simpl
(CT_coerce_PATTERN_to_PATTERN_OPT
(CT_pattern_occ
(CT_int_list(nums_or_var_to_int_list_aux l), xlate_formula c)))
@@ -770,7 +770,7 @@ and xlate_red_tactic =
(match ct_unf_list with
| first :: others -> CT_unfold (CT_unfold_ne_list (first, others))
| [] -> error "there should be at least one thing to unfold")
- | Fold formula_list ->
+ | Fold formula_list ->
CT_fold(CT_formula_list(List.map xlate_formula formula_list))
| Pattern l ->
let pat_list = List.map (fun (occs,c) ->
@@ -782,7 +782,7 @@ and xlate_red_tactic =
| [] -> error "Expecting at least one pattern in a Pattern command")
| ExtraRedExpr _ -> xlate_error "TODO LATER: ExtraRedExpr (probably dead code)"
-and xlate_local_rec_tac = function
+and xlate_local_rec_tac = function
(* TODO LATER: local recursive tactics and global ones should be handled in
the same manner *)
| ((_,x),Tacexp (TacFun (argl,tac))) ->
@@ -797,7 +797,7 @@ and xlate_tactic =
| TacFun (largs, t) ->
let fst, rest = xlate_largs_to_id_opt largs in
CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
- | TacThen (t1,[||],t2,[||]) ->
+ | TacThen (t1,[||],t2,[||]) ->
(match xlate_tactic t1 with
CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
| t -> CT_then (t,[xlate_tactic t2]))
@@ -817,7 +817,7 @@ and xlate_tactic =
| TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
| TacTry t -> CT_try (xlate_tactic t)
| TacRepeat t -> CT_repeat(xlate_tactic t)
- | TacAbstract(t,id_opt) ->
+ | TacAbstract(t,id_opt) ->
CT_abstract((match id_opt with
None -> ctv_ID_OPT_NONE
| Some id -> ctf_ID_OPT_SOME (CT_ident (string_of_id id))),
@@ -827,8 +827,8 @@ and xlate_tactic =
| TacMatch (true,_,_) -> failwith "TODO: lazy match"
| TacMatch (false, exp, rules) ->
CT_match_tac(xlate_tactic exp,
- match List.map
- (function
+ match List.map
+ (function
| Pat ([],p,tac) ->
CT_match_tac_rule(xlate_context_pattern p,
mk_let_value tac)
@@ -836,7 +836,7 @@ and xlate_tactic =
| All tac ->
CT_match_tac_rule
(CT_coerce_FORMULA_to_CONTEXT_PATTERN
- CT_existvarc,
+ CT_existvarc,
mk_let_value tac)) rules with
| [] -> assert false
| fst::others ->
@@ -856,27 +856,27 @@ and xlate_tactic =
CT_coerce_NONE_to_TACTIC_OPT CT_none,
CT_coerce_DEF_BODY_to_LET_VALUE
(formula_to_def_body v))
- | ((_,s),Tacexp t) ->
+ | ((_,s),Tacexp t) ->
CT_let_clause(xlate_ident s,
CT_coerce_NONE_to_TACTIC_OPT CT_none,
CT_coerce_TACTIC_COM_to_LET_VALUE
(xlate_tactic t))
- | ((_,s),t) ->
+ | ((_,s),t) ->
CT_let_clause(xlate_ident s,
CT_coerce_NONE_to_TACTIC_OPT CT_none,
CT_coerce_TACTIC_COM_to_LET_VALUE
(xlate_call_or_tacarg t)) in
let cl_l = List.map cvt_clause l in
(match cl_l with
- | [] -> assert false
+ | [] -> assert false
| fst::others ->
CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t))
| TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition"
- | TacLetIn(true, f1::l, t) ->
+ | TacLetIn(true, f1::l, t) ->
let tl = CT_rec_tactic_fun_list
(xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
CT_rec_tactic_in(tl, xlate_tactic t)
- | TacAtom (_, t) -> xlate_tac t
+ | TacAtom (_, t) -> xlate_tac t
| TacFail (count, []) -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
| TacFail (count, [MsgString s]) -> CT_fail(xlate_id_or_int count,
ctf_STRING_OPT_SOME (CT_string s))
@@ -898,17 +898,17 @@ and xlate_tac =
| Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in
(match l with
[] -> CT_firstorder t1
- | [l1] ->
+ | [l1] ->
(match genarg_tag l1 with
- List1ArgType PreIdentArgType ->
- let l2 = List.map
+ List1ArgType PreIdentArgType ->
+ let l2 = List.map
(fun x -> CT_ident x)
(out_gen (wit_list1 rawwit_pre_ident) l1) in
- let fst,l3 =
+ let fst,l3 =
match l2 with fst::l3 -> fst,l3 | [] -> assert false in
CT_firstorder_using(t1, CT_id_ne_list(fst, l3))
| List1ArgType RefArgType ->
- let l2 = List.map reference_to_ct_ID
+ let l2 = List.map reference_to_ct_ID
(out_gen (wit_list1 rawwit_ref) l1) in
let fst,l3 =
match l2 with fst::l3 -> fst, l3 | [] -> assert false in
@@ -927,11 +927,11 @@ and xlate_tac =
let bindings = xlate_bindings b in
CT_contradiction_thm(c1, bindings))
| TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
- | TacChange (Some(l,c), f, b) ->
+ | TacChange (Some(l,c), f, b) ->
(* TODO LATER: combine with other constructions of pattern_occ *)
let l = nums_of_occs l in
CT_change_local(
- CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l),
+ CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l),
xlate_formula c),
xlate_formula f,
xlate_clause b)
@@ -978,9 +978,9 @@ and xlate_tac =
CT_cofix_tac_list (List.map f cofixtac_list))
| TacMutualCofix (true, id, cofixtac_list) ->
xlate_error "TODO: non user-visible cofix"
- | TacIntrosUntil (NamedHyp id) ->
+ | TacIntrosUntil (NamedHyp id) ->
CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
- | TacIntrosUntil (AnonHyp n) ->
+ | TacIntrosUntil (AnonHyp n) ->
CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n))
| TacIntroMove (Some id1, MoveAfter id2) ->
CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_hyp id2)
@@ -1002,41 +1002,41 @@ and xlate_tac =
| TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
| TacSplit (false,false,[bindl]) -> CT_split (xlate_bindings bindl)
| TacSplit (false,true,[bindl]) -> CT_exists (xlate_bindings bindl)
- | TacSplit _ | TacRight _ | TacLeft _ ->
+ | TacSplit _ | TacRight _ | TacLeft _ ->
xlate_error "TODO: esplit, eright, etc"
| TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
let c1 = xlate_formula (out_gen rawwit_constr c1) in
let c2 = xlate_formula (out_gen rawwit_constr c2) in
- let cl =
- (* J.F. : 18/08/2006
- Hack to coerce the "clause" argument of replace to a real clause
+ let cl =
+ (* J.F. : 18/08/2006
+ Hack to coerce the "clause" argument of replace to a real clause
To be remove if we can reuse the clause grammar entrie defined in g_tactic
*)
- let cl_as_clause = Extraargs.raw_in_arg_hyp_to_clause (out_gen Extraargs.rawwit_in_arg_hyp cl) in
- let cl_as_xlate_arg =
- {cl_as_clause with
- Tacexpr.onhyps =
- Option.map
- (fun l ->
+ let cl_as_clause = Extraargs.raw_in_arg_hyp_to_clause (out_gen Extraargs.rawwit_in_arg_hyp cl) in
+ let cl_as_xlate_arg =
+ {cl_as_clause with
+ Tacexpr.onhyps =
+ Option.map
+ (fun l ->
List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
)
cl_as_clause.Tacexpr.onhyps
}
in
cl_as_xlate_arg
- in
- let cl = xlate_clause cl in
- let tac_opt =
+ in
+ let cl = xlate_clause cl in
+ let tac_opt =
match out_gen (Extraargs.rawwit_by_arg_tac) tac_opt with
| None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
| Some tac ->
let tac = xlate_tactic tac in
CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
- in
+ in
CT_replace_with (c1, c2,cl,tac_opt)
- | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) ->
- let cl = xlate_clause cl
- and c = xlate_formula (fst cbindl)
+ | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) ->
+ let cl = xlate_clause cl
+ and c = xlate_formula (fst cbindl)
and bindl = xlate_bindings (snd cbindl) in
if b then CT_rewrite_lr (c, bindl, cl)
else CT_rewrite_rl (c, bindl, cl)
@@ -1047,7 +1047,7 @@ and xlate_tac =
let b = out_gen Extraargs.rawwit_orient b in
let c = xlate_formula (out_gen rawwit_constr c) in
(match c with
- | CT_coerce_ID_to_FORMULA (CT_ident _ as id) ->
+ | CT_coerce_ID_to_FORMULA (CT_ident _ as id) ->
if b then CT_deprewrite_lr id else CT_deprewrite_rl id
| _ -> xlate_error "dependent rewrite on term: not supported")
| TacExtend (_,"dependent_rewrite", [b; c; id]) ->
@@ -1103,7 +1103,7 @@ and xlate_tac =
match id_list with [] -> assert false | a::tl -> a,tl in
let t1 =
match t with
- [t0] ->
+ [t0] ->
CT_coerce_TACTIC_COM_to_TACTIC_OPT
(xlate_tactic(out_gen rawwit_main_tactic t0))
| [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
@@ -1130,7 +1130,7 @@ and xlate_tac =
second_n,
CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
| Some [] -> CT_eauto(first_n, second_n)
- | Some (a::l) ->
+ | Some (a::l) ->
CT_eauto_with(first_n, second_n,
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR
(CT_id_ne_list
@@ -1141,11 +1141,11 @@ and xlate_tac =
(match out_gen rawwit_int_or_var n with
| ArgVar _ -> xlate_error ""
| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int n))
- (* eapply now represented by TacApply (true,cbindl)
- | TacExtend (_,"eapply", [cbindl]) ->
+ (* eapply now represented by TacApply (true,cbindl)
+ | TacExtend (_,"eapply", [cbindl]) ->
*)
| TacTrivial ([],Some []) -> CT_trivial
- | TacTrivial ([],None) ->
+ | TacTrivial ([],None) ->
CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
| TacTrivial ([],Some (id1::idl)) ->
CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
@@ -1171,7 +1171,7 @@ and xlate_tac =
when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr
& na = Anonymous) cl ->
CT_generalize
- (CT_formula_ne_list (xlate_formula first,
+ (CT_formula_ne_list (xlate_formula first,
List.map (fun ((_,c),_) -> xlate_formula c) cl))
| TacGeneralize _ -> xlate_error "TODO: Generalize at and as"
| TacGeneralizeDep c ->
@@ -1213,7 +1213,7 @@ and xlate_tac =
CT_id_list (List.map xlate_hyp idl))
| TacInversion (DepInversion (k,copt,l),quant_hyp) ->
let id = xlate_quantified_hypothesis quant_hyp in
- CT_depinversion (compute_INV_TYPE k, id,
+ CT_depinversion (compute_INV_TYPE k, id,
xlate_with_names l, xlate_formula_opt copt)
| TacInversion (InversionUsing (c,idlist), id) ->
let id = xlate_quantified_hypothesis id in
@@ -1223,7 +1223,7 @@ and xlate_tac =
| TacRename [id1, id2] -> CT_rename(xlate_hyp id1, xlate_hyp id2)
| TacRename _ -> xlate_error "TODO: add support for n-ary rename"
| TacClearBody([]) -> assert false
- | TacClearBody(a::l) ->
+ | TacClearBody(a::l) ->
CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
| TacDAuto (a, b, []) ->
CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
@@ -1231,39 +1231,39 @@ and xlate_tac =
xlate_error "TODO: dauto using"
| TacInductionDestruct(true,false,[a,b,(None,c),None]) ->
CT_new_destruct
- (List.map xlate_int_or_constr a, xlate_using b,
+ (List.map xlate_int_or_constr a, xlate_using b,
xlate_with_names c)
| TacInductionDestruct(false,false,[a,b,(None,c),None]) ->
CT_new_induction
(List.map xlate_int_or_constr a, xlate_using b,
xlate_with_names c)
- | TacInductionDestruct(_,false,_) ->
+ | TacInductionDestruct(_,false,_) ->
xlate_error "TODO: clause 'in' and full 'as' of destruct/induction"
- | TacLetTac (na, c, cl, true) when cl = nowhere ->
+ | TacLetTac (na, c, cl, true) when cl = nowhere ->
CT_pose(xlate_id_opt_aux na, xlate_formula c)
| TacLetTac (na, c, cl, true) ->
- CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
+ CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c,
(* TODO LATER: This should be shared with Unfold,
but the structures are different *)
xlate_clause cl)
| TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
- | TacAssert (None, Some (_,IntroIdentifier id), c) ->
+ | TacAssert (None, Some (_,IntroIdentifier id), c) ->
CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (None, None, c) ->
+ | TacAssert (None, None, c) ->
CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
- | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) ->
+ | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) ->
CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (Some (TacId []), None, c) ->
+ | TacAssert (Some (TacId []), None, c) ->
CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
| TacAssert _ ->
xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
- | TacAnyConstructor(false,Some tac) ->
+ | TacAnyConstructor(false,Some tac) ->
CT_any_constructor
(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
- | TacAnyConstructor(false,None) ->
+ | TacAnyConstructor(false,None) ->
CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none)
| TacAnyConstructor _ -> xlate_error "TODO: econstructor"
- | TacExtend(_, "ring", [args]) ->
+ | TacExtend(_, "ring", [args]) ->
CT_ring
(CT_formula_list
(List.map xlate_formula
@@ -1328,7 +1328,7 @@ and coerce_genarg_to_TARG x =
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
- | OpenConstrArgType b ->
+ | OpenConstrArgType b ->
CT_coerce_SCOMMENT_CONTENT_to_TARG
(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
(snd (out_gen
@@ -1367,7 +1367,7 @@ and formula_to_def_body =
| ConstrTypeOf f -> CT_type_of (xlate_formula f)
| ConstrTerm c -> ct_coerce_FORMULA_to_DEF_BODY(xlate_formula c)
-and mk_let_value = function
+and mk_let_value = function
TacArg (ConstrMayEval v) ->
CT_coerce_DEF_BODY_to_LET_VALUE(formula_to_def_body v)
| v -> CT_coerce_TACTIC_COM_to_LET_VALUE(xlate_tactic v);;
@@ -1383,7 +1383,7 @@ let coerce_genarg_to_VARG x =
(CT_coerce_INT_to_INT_OPT (CT_int n)))
| IntOrVarArgType ->
(match out_gen rawwit_int_or_var x with
- | ArgArg n ->
+ | ArgArg n ->
CT_coerce_ID_OR_INT_OPT_to_VARG
(CT_coerce_INT_OPT_to_ID_OR_INT_OPT
(CT_coerce_INT_to_INT_OPT (CT_int n)))
@@ -1420,11 +1420,11 @@ let coerce_genarg_to_VARG x =
(CT_coerce_ID_to_ID_OPT id))
(* Specific types *)
| SortArgType ->
- CT_coerce_FORMULA_OPT_to_VARG
+ CT_coerce_FORMULA_OPT_to_VARG
(CT_coerce_FORMULA_to_FORMULA_OPT
(CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x))))
| ConstrArgType ->
- CT_coerce_FORMULA_OPT_to_VARG
+ CT_coerce_FORMULA_OPT_to_VARG
(CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
| ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
| QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
@@ -1529,8 +1529,8 @@ let cvt_optional_eval_for_definition c1 optional_eval =
let cvt_vernac_binder = function
| b,(id::idl,c) ->
- let l,t =
- CT_id_opt_ne_list
+ let l,t =
+ CT_id_opt_ne_list
(xlate_ident_opt (Some (snd id)),
List.map (fun id -> xlate_ident_opt (Some (snd id))) idl),
xlate_formula c in
@@ -1556,8 +1556,8 @@ let xlate_comment = function
let translate_opt_notation_decl = function
None -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none)
| Some(s, f, sc) ->
- let tr_sc =
- match sc with
+ let tr_sc =
+ match sc with
None -> ctv_ID_OPT_NONE
| Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in
CT_decl_notation(CT_string s, xlate_formula f, tr_sc);;
@@ -1588,18 +1588,18 @@ let xlate_syntax_modifier = function
let rec xlate_module_type = function
- | CMTEident(_, qid) ->
+ | CMTEident(_, qid) ->
CT_coerce_ID_to_MODULE_TYPE(CT_ident (xlate_qualid qid))
| CMTEwith(mty, decl) ->
let mty1 = xlate_module_type mty in
(match decl with
CWith_Definition((_, idl), c) ->
- CT_module_type_with_def(mty1,
+ CT_module_type_with_def(mty1,
CT_id_list (List.map xlate_ident idl),
xlate_formula c)
| CWith_Module((_, idl), (_, qid)) ->
CT_module_type_with_mod(mty1,
- CT_id_list (List.map xlate_ident idl),
+ CT_id_list (List.map xlate_ident idl),
CT_ident (xlate_qualid qid)))
| CMTEapply (_,_) -> xlate_error "TODO: Funsig application";;
@@ -1607,7 +1607,7 @@ let rec xlate_module_type = function
let xlate_module_binder_list (l:module_binder list) =
CT_module_binder_list
(List.map (fun (_, idl, mty) ->
- let idl1 =
+ let idl1 =
List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in
let fst,idl2 = match idl1 with
[] -> assert false
@@ -1619,7 +1619,7 @@ let xlate_module_type_check_opt = function
None -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
(CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE)
| Some(mty, true) -> CT_only_check(xlate_module_type mty)
- | Some(mty, false) ->
+ | Some(mty, false) ->
CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
(CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
(xlate_module_type mty));;
@@ -1633,7 +1633,7 @@ let rec xlate_module_expr = function
let rec xlate_vernac =
function
| VernacDeclareTacticDefinition (true, tacs) ->
- (match List.map
+ (match List.map
(function
(id, _, body) ->
CT_tac_def(reference_to_ct_ID id, xlate_tactic body))
@@ -1642,7 +1642,7 @@ let rec xlate_vernac =
| fst::tacs1 ->
CT_tactic_definition
(CT_tac_def_ne_list(fst, tacs1)))
- | VernacDeclareTacticDefinition(false, _) ->
+ | VernacDeclareTacticDefinition(false, _) ->
xlate_error "obsolete tactic definition not handled"
| VernacLoad (verbose,s) ->
CT_load (
@@ -1682,14 +1682,14 @@ let rec xlate_vernac =
| VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
| VernacAbortAll -> CT_abort ctv_ID_OPT_OR_ALL_ALL
| VernacRestart -> CT_restart
- | VernacSolve (n, tac, b) ->
+ | VernacSolve (n, tac, b) ->
CT_solve (CT_int n, xlate_tactic tac,
if b then CT_dotdot
else CT_coerce_NONE_to_DOTDOT_OPT CT_none)
(* MMode *)
- | (VernacDeclProof | VernacReturn | VernacProofInstr _) ->
+ | (VernacDeclProof | VernacReturn | VernacProofInstr _) ->
anomaly "No MMode in CTcoq"
@@ -1701,7 +1701,7 @@ let rec xlate_vernac =
let file = out_gen rawwit_string f in
let l1 = out_gen (wit_list1 rawwit_ref) l in
let fst,l2 = match l1 with [] -> assert false | fst::l2 -> fst, l2 in
- CT_extract_to_file(CT_string file,
+ CT_extract_to_file(CT_string file,
CT_id_ne_list(loc_qualid_to_ct_ID fst,
List.map loc_qualid_to_ct_ID l2))
| VernacExtend("ExtractionInline", [l]) ->
@@ -1714,7 +1714,7 @@ let rec xlate_vernac =
let fst, l2 = match l1 with [] -> assert false | fst ::l2 -> fst, l2 in
CT_no_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
List.map loc_qualid_to_ct_ID l2))
- | VernacExtend("Field",
+ | VernacExtend("Field",
[fth;ainv;ainvl;div]) ->
(match List.map (fun v -> xlate_formula(out_gen rawwit_constr v))
[fth;ainv;ainvl]
@@ -1728,7 +1728,7 @@ let rec xlate_vernac =
let orient = out_gen Extraargs.rawwit_orient o in
let formula_list = out_gen (wit_list1 rawwit_constr) f in
let base = out_gen rawwit_pre_ident b in
- let t =
+ let t =
match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId []
in
let ct_orient = match orient with
@@ -1754,17 +1754,17 @@ let rec xlate_vernac =
CT_hints(CT_ident "Constructors",
CT_id_ne_list(n1, names), dblist)
| HintsExtern (n, c, t) ->
- let pat = match c with
+ let pat = match c with
| None -> CT_coerce_ID_OPT_to_FORMULA_OPT (CT_coerce_NONE_to_ID_OPT CT_none)
- | Some c -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula c)
+ | Some c -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula c)
in CT_hint_extern(CT_int n, pat, xlate_tactic t, dblist)
- | HintsImmediate l ->
+ | HintsImmediate l ->
let f1, formulas = match List.map xlate_formula l with
a :: tl -> a, tl
| _ -> failwith "" in
let l' = CT_formula_ne_list(f1, formulas) in
if local then
- (match h with
+ (match h with
HintsResolve _ ->
CT_local_hints_resolve(l', dblist)
| HintsImmediate _ ->
@@ -1775,13 +1775,13 @@ let rec xlate_vernac =
HintsResolve _ -> CT_hints_resolve(l', dblist)
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
| _ -> assert false)
- | HintsResolve l ->
+ | HintsResolve l ->
let f1, formulas = match List.map xlate_formula (List.map pi3 l) with
a :: tl -> a, tl
| _ -> failwith "" in
let l' = CT_formula_ne_list(f1, formulas) in
if local then
- (match h with
+ (match h with
HintsResolve _ ->
CT_local_hints_resolve(l', dblist)
| HintsImmediate _ ->
@@ -1792,16 +1792,16 @@ let rec xlate_vernac =
HintsResolve _ -> CT_hints_resolve(l', dblist)
| HintsImmediate _ -> CT_hints_immediate(l', dblist)
| _ -> assert false)
- | HintsUnfold l ->
+ | HintsUnfold l ->
let n1, names = match List.map loc_qualid_to_ct_ID l with
n1 :: names -> n1, names
| _ -> failwith "" in
if local then
CT_local_hints(CT_ident "Unfold",
CT_id_ne_list(n1, names), dblist)
- else
+ else
CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)
- | HintsTransparency (l,b) ->
+ | HintsTransparency (l,b) ->
let n1, names = match List.map loc_qualid_to_ct_ID l with
n1 :: names -> n1, names
| _ -> failwith "" in
@@ -1809,7 +1809,7 @@ let rec xlate_vernac =
if local then
CT_local_hints(CT_ident ty,
CT_id_ne_list(n1, names), dblist)
- else
+ else
CT_hints(CT_ident ty, CT_id_ne_list(n1, names), dblist)
| HintsDestruct(id, n, loc, f, t) ->
let dl = match loc with
@@ -1869,9 +1869,9 @@ let rec xlate_vernac =
| PrintModules -> CT_print_modules
| PrintGrammar name -> CT_print_grammar CT_grammar_none
| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
- | PrintHintDbName id ->
+ | PrintHintDbName id ->
CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
- | PrintRewriteHintDbName id ->
+ | PrintRewriteHintDbName id ->
CT_print_rewrite_hintdb (CT_ident id)
| PrintHint id ->
CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_smart_global_to_ct_ID id))
@@ -1884,15 +1884,15 @@ let rec xlate_vernac =
| PrintClasses -> CT_print_classes
| PrintLtac qid -> CT_print_ltac (loc_qualid_to_ct_ID qid)
| PrintCoercions -> CT_print_coercions
- | PrintCoercionPaths (id1, id2) ->
+ | PrintCoercionPaths (id1, id2) ->
CT_print_path (xlate_class id1, xlate_class id2)
| PrintCanonicalConversions ->
xlate_error "TODO: Print Canonical Structures"
- | PrintAssumptions _ ->
+ | PrintAssumptions _ ->
xlate_error "TODO: Print Needed Assumptions"
- | PrintInstances _ ->
+ | PrintInstances _ ->
xlate_error "TODO: Print Instances"
- | PrintTypeClasses ->
+ | PrintTypeClasses ->
xlate_error "TODO: Print TypeClasses"
| PrintInspect n -> CT_inspect (CT_int n)
| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
@@ -1902,7 +1902,7 @@ let rec xlate_vernac =
| PrintScopes -> CT_print_scopes
| PrintScope id -> CT_print_scope (CT_ident id)
| PrintVisibility id_opt ->
- CT_print_visibility
+ CT_print_visibility
(match id_opt with
Some id -> CT_coerce_ID_to_ID_OPT(CT_ident id)
| None -> ctv_ID_OPT_NONE)
@@ -1947,9 +1947,9 @@ let rec xlate_vernac =
let xlate_search_about_item (b,it) =
if not b then xlate_error "TODO: negative searchabout constraint";
match it with
- SearchSubPattern (CRef x) ->
+ SearchSubPattern (CRef x) ->
CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
- | SearchString (s,None) ->
+ | SearchString (s,None) ->
CT_coerce_STRING_to_ID_OR_STRING(CT_string s)
| SearchString _ | SearchSubPattern _ ->
xlate_error
@@ -1992,7 +1992,7 @@ let rec xlate_vernac =
let ardef = xlate_formula ardef in
match xlate_binder_list bl with
| CT_binder_list (b :: bl) ->
- CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
+ CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
struct_arg, arf, ardef)
| _ -> xlate_error "mutual recursive" in
CT_fix_decl
@@ -2009,7 +2009,7 @@ let rec xlate_vernac =
let strip_ind = function
| (Some (_,id), InductionScheme (depstr, inde, sort)) ->
CT_scheme_spec
- (xlate_ident id, xlate_dep depstr,
+ (xlate_ident id, xlate_dep depstr,
CT_coerce_ID_to_FORMULA (loc_smart_global_to_ct_ID inde),
xlate_sort sort)
| (None, InductionScheme (depstr, inde, sort)) ->
@@ -2027,7 +2027,7 @@ let rec xlate_vernac =
xlate_error"TODO: Local abbreviations and abbreviations with parameters"
(* Modules and Module Types *)
| VernacInclude (_) -> xlate_error "TODO : Include "
- | VernacDeclareModuleType((_, id), bl, mty_o) ->
+ | VernacDeclareModuleType((_, id), bl, mty_o) ->
CT_module_type_decl(xlate_ident id,
xlate_module_binder_list bl,
match mty_o with
@@ -2038,20 +2038,20 @@ let rec xlate_vernac =
CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
(xlate_module_type mty1))
| VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
- CT_module(xlate_ident id,
+ CT_module(xlate_ident id,
xlate_module_binder_list bl,
xlate_module_type_check_opt mty_o,
match mexpr_o with
None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
| Some m -> xlate_module_expr m)
- | VernacDeclareModule(_,(_, id), bl, mty_o) ->
- CT_declare_module(xlate_ident id,
+ | VernacDeclareModule(_,(_, id), bl, mty_o) ->
+ CT_declare_module(xlate_ident id,
xlate_module_binder_list bl,
xlate_module_type_check_opt (Some mty_o),
CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
| VernacRequire (impexp, spec, id::idl) ->
let ct_impexp, ct_spec = get_require_flags impexp spec in
- CT_require (ct_impexp, ct_spec,
+ CT_require (ct_impexp, ct_spec,
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STRING(
CT_id_ne_list(loc_qualid_to_ct_ID id,
List.map loc_qualid_to_ct_ID idl)))
@@ -2059,14 +2059,14 @@ let rec xlate_vernac =
xlate_error "Require should have at least one id argument"
| VernacRequireFrom (impexp, spec, filename) ->
let ct_impexp, ct_spec = get_require_flags impexp spec in
- CT_require(ct_impexp, ct_spec,
+ CT_require(ct_impexp, ct_spec,
CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
| VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
| VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
| VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
| VernacOpenCloseScope(false, false, s) -> CT_close_scope(CT_ident s)
- | VernacArgumentsScope(true, qid, l) ->
+ | VernacArgumentsScope(true, qid, l) ->
CT_arguments_scope(loc_smart_global_to_ct_ID qid,
CT_id_opt_list
(List.map
@@ -2074,10 +2074,10 @@ let rec xlate_vernac =
match x with
None -> ctv_ID_OPT_NONE
| Some x -> ctf_ID_OPT_SOME(CT_ident x)) l))
- | VernacArgumentsScope(false, qid, l) ->
+ | VernacArgumentsScope(false, qid, l) ->
xlate_error "TODO: Arguments Scope Global"
| VernacDelimiters(s1,s2) -> CT_delim_scope(CT_ident s1, CT_ident s2)
- | VernacBindScope(id, a::l) ->
+ | VernacBindScope(id, a::l) ->
let xlate_class_rawexpr = function
FunClass -> CT_ident "Funclass" | SortClass -> CT_ident "Sortclass"
| RefClass qid -> loc_smart_global_to_ct_ID qid in
@@ -2085,10 +2085,10 @@ let rec xlate_vernac =
CT_id_ne_list(xlate_class_rawexpr a,
List.map xlate_class_rawexpr l))
| VernacBindScope(id, []) -> assert false
- | VernacNotation(b, c, (s,modif_list), opt_scope) ->
+ | VernacNotation(b, c, (s,modif_list), opt_scope) ->
let translated_s = CT_string s in
let formula = xlate_formula c in
- let translated_modif_list =
+ let translated_modif_list =
CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
let translated_scope = match opt_scope with
None -> ctv_ID_OPT_NONE
@@ -2097,11 +2097,11 @@ let rec xlate_vernac =
CT_local_define_notation
(translated_s, formula, translated_modif_list, translated_scope)
else
- CT_define_notation(translated_s, formula,
+ CT_define_notation(translated_s, formula,
translated_modif_list, translated_scope)
- | VernacSyntaxExtension(b,(s,modif_list)) ->
+ | VernacSyntaxExtension(b,(s,modif_list)) ->
let translated_s = CT_string s in
- let translated_modif_list =
+ let translated_modif_list =
CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
if b then
CT_local_reserve_notation(translated_s, translated_modif_list)
@@ -2118,7 +2118,7 @@ let rec xlate_vernac =
CT_local_infix(s, id1,modl1, translated_scope)
else
CT_infix(s, id1,modl1, translated_scope)
- | VernacInfix (b,(str,modl),_ , opt_scope) ->
+ | VernacInfix (b,(str,modl),_ , opt_scope) ->
xlate_error "TODO: Infix not ref"
| VernacCoercion (s, id1, id2, id3) ->
let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
@@ -2140,7 +2140,7 @@ let rec xlate_vernac =
CT_coercion (local_opt, id_opt, xlate_ident id1,
xlate_class id2, xlate_class id3)
- (* Type Classes *)
+ (* Type Classes *)
| VernacDeclareInstance _|VernacContext _|
VernacInstance (_, _, _, _, _) ->
xlate_error "TODO: Type Classes commands"
@@ -2150,20 +2150,20 @@ let rec xlate_vernac =
| VernacExtend (s, l) ->
CT_user_vernac
(CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
- | VernacList((_, a)::l) ->
+ | VernacList((_, a)::l) ->
CT_coerce_COMMAND_LIST_to_COMMAND
- (CT_command_list(xlate_vernac a,
+ (CT_command_list(xlate_vernac a,
List.map (fun (_, x) -> xlate_vernac x) l))
| VernacList([]) -> assert false
| VernacNop -> CT_proof_no_op
- | VernacComments l ->
+ | VernacComments l ->
CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
| VernacDeclareImplicits(true, id, opt_positions) ->
CT_implicits
(loc_smart_global_to_ct_ID id,
match opt_positions with
None -> CT_coerce_NONE_to_ID_LIST_OPT CT_none
- | Some l ->
+ | Some l ->
CT_coerce_ID_LIST_to_ID_LIST_OPT
(CT_id_list
(List.map
@@ -2174,7 +2174,7 @@ let rec xlate_vernac =
| VernacDeclareImplicits(false, id, opt_positions) ->
xlate_error "TODO: Implicit Arguments Global"
| VernacReserve((_,a)::l, f) ->
- CT_reserve(CT_id_ne_list(xlate_ident a,
+ CT_reserve(CT_id_ne_list(xlate_ident a,
List.map (fun (_,x) -> xlate_ident x) l),
xlate_formula f)
| VernacReserve([], _) -> assert false
@@ -2186,15 +2186,15 @@ let rec xlate_vernac =
| VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v)
| VernacSetOption (_,["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
|VernacExactProof f -> CT_proof(xlate_formula f)
- | VernacSetOption (_,table, BoolValue true) ->
- let table1 =
+ | VernacSetOption (_,table, BoolValue true) ->
+ let table1 =
match table with
[s] -> CT_coerce_ID_to_TABLE(CT_ident s)
| [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
| _ -> xlate_error "TODO: arbitrary-length Table names" in
CT_set_option(table1)
- | VernacSetOption (_,table, v) ->
- let table1 =
+ | VernacSetOption (_,table, v) ->
+ let table1 =
match table with
[s] -> CT_coerce_ID_to_TABLE(CT_ident s)
| [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
@@ -2208,7 +2208,7 @@ let rec xlate_vernac =
CT_coerce_INT_to_SINGLE_OPTION_VALUE(CT_int n) in
CT_set_option_value(table1, value)
| VernacUnsetOption(_,table) ->
- let table1 =
+ let table1 =
match table with
[s] -> CT_coerce_ID_to_TABLE(CT_ident s)
| [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
@@ -2218,13 +2218,13 @@ let rec xlate_vernac =
let values =
List.map
(function
- | QualidRefValue x ->
+ | QualidRefValue x ->
CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
- | StringRefValue x ->
+ | StringRefValue x ->
CT_coerce_STRING_to_ID_OR_STRING(CT_string x)) l in
- let fst, values1 =
+ let fst, values1 =
match values with [] -> assert false | a::b -> (a,b) in
- let table1 =
+ let table1 =
match table with
[s] -> CT_coerce_ID_to_TABLE(CT_ident s)
| [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:45:24 +0000