aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
authorglondu2009-09-17 15:58:14 +0000
committerglondu2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/subtac
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/equations.ml4354
-rw-r--r--plugins/subtac/eterm.ml94
-rw-r--r--plugins/subtac/eterm.mli8
-rw-r--r--plugins/subtac/g_eterm.ml42
-rw-r--r--plugins/subtac/g_subtac.ml430
-rw-r--r--plugins/subtac/subtac.ml82
-rw-r--r--plugins/subtac/subtac_cases.ml324
-rw-r--r--plugins/subtac/subtac_classes.ml58
-rw-r--r--plugins/subtac/subtac_classes.mli2
-rw-r--r--plugins/subtac/subtac_coercion.ml142
-rw-r--r--plugins/subtac/subtac_command.ml132
-rw-r--r--plugins/subtac/subtac_command.mli2
-rw-r--r--plugins/subtac/subtac_errors.ml6
-rw-r--r--plugins/subtac/subtac_obligations.ml208
-rw-r--r--plugins/subtac/subtac_obligations.mli14
-rw-r--r--plugins/subtac/subtac_pretyping.ml22
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml130
-rw-r--r--plugins/subtac/subtac_utils.ml112
-rw-r--r--plugins/subtac/subtac_utils.mli4
-rw-r--r--plugins/subtac/test/ListDep.v8
-rw-r--r--plugins/subtac/test/ListsTest.v18
-rw-r--r--plugins/subtac/test/Mutind.v4
-rw-r--r--plugins/subtac/test/Test1.v2
-rw-r--r--plugins/subtac/test/euclid.v4
-rw-r--r--plugins/subtac/test/take.v2
-rw-r--r--plugins/subtac/test/wf.v2
26 files changed, 883 insertions, 883 deletions
diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4
index 5ae15e00a1..ca4445cc2e 100644
--- a/plugins/subtac/equations.ml4
+++ b/plugins/subtac/equations.ml4
@@ -8,7 +8,7 @@
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
(* $Id$ *)
@@ -40,18 +40,18 @@ type pat =
| PInac of constr
let coq_inacc = lazy (Coqlib.gen_constant "equations" ["Program";"Equality"] "inaccessible_pattern")
-
+
let mkInac env c =
mkApp (Lazy.force coq_inacc, [| Typing.type_of env Evd.empty c ; c |])
-
+
let rec constr_of_pat ?(inacc=true) env = function
| PRel i -> mkRel i
- | PCstr (c, p) ->
+ | PCstr (c, p) ->
let c' = mkConstruct c in
mkApp (c', Array.of_list (constrs_of_pats ~inacc env p))
- | PInac r ->
+ | PInac r ->
if inacc then try mkInac env r with _ -> r else r
-
+
and constrs_of_pats ?(inacc=true) env l = map (constr_of_pat ~inacc env) l
let rec pat_vars = function
@@ -59,8 +59,8 @@ let rec pat_vars = function
| PCstr (c, p) -> pats_vars p
| PInac _ -> Intset.empty
-and pats_vars l =
- fold_left (fun vars p ->
+and pats_vars l =
+ fold_left (fun vars p ->
let pvars = pat_vars p in
let inter = Intset.inter pvars vars in
if inter = Intset.empty then
@@ -70,7 +70,7 @@ and pats_vars l =
Intset.empty l
let rec pats_of_constrs l = map pat_of_constr l
-and pat_of_constr c =
+and pat_of_constr c =
match kind_of_term c with
| Rel i -> PRel i
| App (f, [| a ; c |]) when eq_constr f (Lazy.force coq_inacc) ->
@@ -95,10 +95,10 @@ let rec pmatch p c =
and pmatches pl l =
match pl, l with
| [], [] -> []
- | hd :: tl, hd' :: tl' ->
+ | hd :: tl, hd' :: tl' ->
pmatch hd hd' @ pmatches tl tl'
| _ -> raise Conflict
-
+
let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None
let rec pinclude p c =
@@ -108,59 +108,59 @@ let rec pinclude p c =
| PInac _, _ -> true
| _, PInac _ -> true
| _, _ -> false
-
+
and pincludes pl l =
match pl, l with
| [], [] -> true
- | hd :: tl, hd' :: tl' ->
+ | hd :: tl, hd' :: tl' ->
pinclude hd hd' && pincludes tl tl'
| _ -> false
-
+
let pattern_includes pl l = pincludes pl l
(** Specialize by a substitution. *)
let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s)
-let subst_rel_subst k s c =
+let subst_rel_subst k s c =
let rec aux depth c =
match kind_of_term c with
- | Rel n ->
- let k = n - depth in
- if k >= 0 then
+ | Rel n ->
+ let k = n - depth in
+ if k >= 0 then
try lift depth (snd (assoc k s))
with Not_found -> c
else c
| _ -> map_constr_with_binders succ aux depth c
in aux k c
-
+
let subst_context s ctx =
- let (_, ctx') = fold_right
+ let (_, ctx') = fold_right
(fun (id, b, t) (k, ctx') ->
(succ k, (id, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx'))
ctx (0, [])
in ctx'
-let subst_rel_context k cstr ctx =
- let (_, ctx') = fold_right
+let subst_rel_context k cstr ctx =
+ let (_, ctx') = fold_right
(fun (id, b, t) (k, ctx') ->
(succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
ctx (k, [])
in ctx'
-let rec lift_pat n k p =
+let rec lift_pat n k p =
match p with
| PRel i ->
if i >= k then PRel (i + n)
else p
| PCstr(c, pl) -> PCstr (c, lift_pats n k pl)
| PInac r -> PInac (liftn n k r)
-
+
and lift_pats n k = map (lift_pat n k)
-let rec subst_pat env k t p =
+let rec subst_pat env k t p =
match p with
- | PRel i ->
+ | PRel i ->
if i = k then t
else if i > k then PRel (pred i)
else p
@@ -170,9 +170,9 @@ let rec subst_pat env k t p =
and subst_pats env k t = map (subst_pat env k t)
-let rec specialize s p =
+let rec specialize s p =
match p with
- | PRel i ->
+ | PRel i ->
if mem_assoc i s then
let b, t = assoc i s in
if b then PInac t
@@ -190,10 +190,10 @@ let specialize_patterns = function
| s -> specialize_pats s
let specialize_rel_context s ctx =
- snd (fold_right (fun (n, b, t) (k, ctx) ->
+ snd (fold_right (fun (n, b, t) (k, ctx) ->
(succ k, (n, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx))
ctx (0, []))
-
+
let lift_contextn n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
@@ -202,7 +202,7 @@ let lift_contextn n k sign =
in
liftrec (rel_context_length sign + k) sign
-type program =
+type program =
signature * clause list
and signature = identifier * rel_context * constr
@@ -211,16 +211,16 @@ and clause = lhs * (constr, int) rhs
and lhs = rel_context * identifier * pat list
-and ('a, 'b) rhs =
+and ('a, 'b) rhs =
| Program of 'a
| Empty of 'b
-type splitting =
+type splitting =
| Compute of clause
| Split of lhs * int * inductive_family *
unification_result array * splitting option array
-
-and unification_result =
+
+and unification_result =
rel_context * int * constr * pat * substitution option
and substitution = (int * (bool * constr)) list
@@ -236,14 +236,14 @@ let split_solves split prob =
| Compute (lhs, rhs) -> lhs = prob
| Split (lhs, id, indf, us, ls) -> lhs = prob
-let ids_of_constr c =
- let rec aux vars c =
+let ids_of_constr c =
+ let rec aux vars c =
match kind_of_term c with
| Var id -> Idset.add id vars
| _ -> fold_constr aux vars c
in aux Idset.empty c
-let ids_of_constrs =
+let ids_of_constrs =
fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty
let idset_of_list =
@@ -252,8 +252,8 @@ let idset_of_list =
let intset_of_list =
fold_left (fun s x -> Intset.add x s) Intset.empty
-let solves split (delta, id, pats as prob) =
- split_solves split prob &&
+let solves split (delta, id, pats as prob) =
+ split_solves split prob &&
Intset.equal (pats_vars pats) (intset_of_list (map destRel (rels_of_tele delta)))
let check_judgment ctx c t =
@@ -261,7 +261,7 @@ let check_judgment ctx c t =
let check_context env ctx =
fold_right
- (fun (_, _, t as decl) env ->
+ (fun (_, _, t as decl) env ->
ignore(Typing.sort_of env Evd.empty t); push_rel decl env)
ctx env
@@ -270,7 +270,7 @@ let split_context n c =
match before with
| hd :: tl -> after, hd, tl
| [] -> raise (Invalid_argument "split_context")
-
+
let split_tele n (ctx : rel_context) =
let rec aux after n l =
match n, l with
@@ -284,12 +284,12 @@ let rec add_var_subst env subst n c =
let t = assoc n subst in
if eq_constr t c then subst
else unify env subst t c
- else
+ else
let rel = mkRel n in
if rel = c then subst
else if dependent rel c then raise Conflict
else (n, c) :: subst
-
+
and unify env subst x y =
match kind_of_term x, kind_of_term y with
| Rel n, _ -> add_var_subst env subst n y
@@ -298,7 +298,7 @@ and unify env subst x y =
unify_constrs env subst (Array.to_list l) (Array.to_list l')
| _, _ -> if eq_constr x y then subst else raise Conflict
-and unify_constrs (env : env) subst l l' =
+and unify_constrs (env : env) subst l l' =
if List.length l = List.length l' then
fold_left2 (unify env) subst l l'
else raise Conflict
@@ -306,10 +306,10 @@ and unify_constrs (env : env) subst l l' =
let fold_rel_context_with_binders f ctx init =
snd (List.fold_right (fun decl (depth, acc) ->
(succ depth, f depth decl acc)) ctx (0, init))
-
+
let dependent_rel_context (ctx : rel_context) k =
fold_rel_context_with_binders
- (fun depth (n,b,t) acc ->
+ (fun depth (n,b,t) acc ->
let r = mkRel (depth + k) in
acc || dependent r t ||
(match b with
@@ -319,14 +319,14 @@ let dependent_rel_context (ctx : rel_context) k =
let liftn_between n k p c =
let rec aux depth c = match kind_of_term c with
- | Rel i ->
+ | Rel i ->
if i <= depth then c
else if i-depth > p then c
else mkRel (i - n)
| _ -> map_constr_with_binders succ aux depth c
in aux k c
-
-let liftn_rel_context n k sign =
+
+let liftn_rel_context n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
@@ -348,7 +348,7 @@ let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list
let s = rev s in
let s' = map (fun (korig, (b, knew)) -> korig, (b, substl s knew)) subst in
s', ctx'
-
+
(* Compute the transitive closure of the dependency relation for a term in a context *)
let rec dependencies_of_rel ctx k =
@@ -356,12 +356,12 @@ let rec dependencies_of_rel ctx k =
let b = Option.map (lift k) b and t = lift k t in
let bdeps = match b with Some b -> dependencies_of_term ctx b | None -> Intset.empty in
Intset.union (Intset.singleton k) (Intset.union bdeps (dependencies_of_term ctx t))
-
+
and dependencies_of_term ctx t =
let rels = free_rels t in
Intset.fold (fun i -> Intset.union (dependencies_of_rel ctx i)) rels Intset.empty
-let subst_telescope k cstr ctx =
+let subst_telescope k cstr ctx =
let (_, ctx') = fold_left
(fun (k, ctx') (id, b, t) ->
(succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
@@ -374,9 +374,9 @@ let lift_telescope n k sign =
(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (succ k) sign)
| [] -> []
in liftrec k sign
-
+
type ('a,'b) either = Inl of 'a | Inr of 'b
-
+
let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list =
let rels = dependencies_of_term ctx t in
let len = length ctx in
@@ -390,7 +390,7 @@ let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (i
else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx'
| [] -> rev acc, rev rest, s
in aux 1 1 [] 1 [] [] ctx
-
+
let merge_subst (ctx', rest, s) =
let lenrest = length rest in
map (function (k, Inl x) -> (k, (false, mkRel (x + lenrest))) | (k, Inr x) -> k, (false, mkRel x)) s
@@ -412,7 +412,7 @@ let substitute_in_ctx n c ctx =
if k = n then rev after @ (name, Some c, t) :: before
else aux (succ k) (decl :: after) before
in aux 1 [] ctx
-
+
let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) list) (cursubst : (int * (bool * constr)) list) =
match cursubst with
| [] -> ctx, substacc
@@ -423,7 +423,7 @@ let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) lis
let t' = lift (-k) t in
let ctx' = substitute_in_ctx k t' ctx in
reduce_subst ctx' substacc rest
- else (* The term refers to variables declared after [k], so we have
+ else (* The term refers to variables declared after [k], so we have
to move these dependencies before [k]. *)
let (minctx, ctxrest, subst as str) = strengthen ctx t in
match assoc k subst with
@@ -439,8 +439,8 @@ let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) lis
in map substsubst ((k, (b, t)) :: rest)
in
reduce_subst ctx' (compose_subst s substacc) rest' (* (compose_subst s ((k, (b, t)) :: rest)) *)
-
-
+
+
let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
let _, subst =
fold_left (fun (k, s) _ ->
@@ -452,7 +452,7 @@ let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
in
let ctx', subst' = reduce_subst ctx subst subst in
reduce_rel_context ctx' subst'
-
+
let unify_type before ty =
try
let envb = push_rel_context before (Global.env()) in
@@ -460,11 +460,11 @@ let unify_type before ty =
let ind, params = dest_ind_family indf in
let vs = map (Reduction.whd_betadeltaiota envb) args in
let cstrs = Inductiveops.arities_of_constructors envb ind in
- let cstrs =
+ let cstrs =
Array.mapi (fun i ty ->
let ty = prod_applist ty params in
let ctx, ty = decompose_prod_assum ty in
- let ctx, ids =
+ let ctx, ids =
let ids = ids_of_rel_context ctx in
fold_right (fun (n, b, t as decl) (acc, ids) ->
match n with Name _ -> (decl :: acc), ids
@@ -480,8 +480,8 @@ let unify_type before ty =
env', ctx, constr, constrpat, (* params @ *)args)
cstrs
in
- let res =
- Array.map (fun (env', ctxc, c, cpat, us) ->
+ let res =
+ Array.map (fun (env', ctxc, c, cpat, us) ->
let _beforelen = length before and ctxclen = length ctxc in
let fullctx = ctxc @ before in
try
@@ -490,7 +490,7 @@ let unify_type before ty =
let subst = unify_constrs fullenv [] vs' us in
let subst', ctx' = substituted_context subst fullctx in
(ctx', ctxclen, c, cpat, Some subst')
- with Conflict ->
+ with Conflict ->
(fullctx, ctxclen, c, cpat, None)) cstrs
in Some (res, indf)
with Not_found -> (* not an inductive type *)
@@ -502,35 +502,35 @@ let rec id_of_rel n l =
| n, _ :: tl -> id_of_rel (pred n) tl
| _, _ -> raise (Invalid_argument "id_of_rel")
-let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) =
+let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) =
constrs_of_pats ~inacc (push_rel_context ctx env) pats
-
-let rec valid_splitting (f, delta, t, pats) tree =
- split_solves tree (delta, f, pats) &&
+
+let rec valid_splitting (f, delta, t, pats) tree =
+ split_solves tree (delta, f, pats) &&
valid_splitting_tree (f, delta, t) tree
-
+
and valid_splitting_tree (f, delta, t) = function
- | Compute (lhs, Program rhs) ->
- let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in
+ | Compute (lhs, Program rhs) ->
+ let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in
ignore(check_judgment (pi1 lhs) rhs (substl subst t)); true
- | Compute ((ctx, id, lhs), Empty split) ->
+ | Compute ((ctx, id, lhs), Empty split) ->
let before, (x, _, ty), after = split_context split ctx in
- let unify =
+ let unify =
match unify_type before ty with
- | Some (unify, _) -> unify
+ | Some (unify, _) -> unify
| None -> assert false
in
array_for_all (fun (_, _, _, _, x) -> x = None) unify
-
- | Split ((ctx, id, lhs), rel, indf, unifs, ls) ->
+
+ | Split ((ctx, id, lhs), rel, indf, unifs, ls) ->
let before, (id, _, ty), after = split_tele (pred rel) ctx in
let unify, indf' = Option.get (unify_type before ty) in
assert(indf = indf');
if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false
else
- let ok, splits =
- Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) ->
+ let ok, splits =
+ Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) ->
match subst with
| None -> acc
| Some subst ->
@@ -540,23 +540,23 @@ and valid_splitting_tree (f, delta, t) = function
(* ignore(check_context env' (subst_context subst before)); *)
(* true *)
(* in *)
- let newdelta =
- subst_context subst (subst_rel_context 0 cstr
+ let newdelta =
+ subst_context subst (subst_rel_context 0 cstr
(lift_contextn ctxlen 0 after)) @ before in
let liftpats = lift_pats ctxlen rel lhs in
let newpats = specialize_patterns subst (subst_pats (Global.env ()) rel cstrpat liftpats) in
(ok, (f, newdelta, newpats) :: splits))
(true, []) unify
in
- let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta
- (constrs_of_pats ~inacc:false (Global.env ()) lhs)
+ let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta
+ (constrs_of_pats ~inacc:false (Global.env ()) lhs)
in
let t' = replace_vars subst t in
- ok && for_all
- (fun (f, delta', pats') ->
+ ok && for_all
+ (fun (f, delta', pats') ->
array_exists (function None -> false | Some tree -> valid_splitting (f, delta', t', pats') tree) ls) splits
-
-let valid_tree (f, delta, t) tree =
+
+let valid_tree (f, delta, t) tree =
valid_splitting (f, delta, t, patvars_of_tele delta) tree
let is_constructor c =
@@ -579,12 +579,12 @@ let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) =
and find_split_pats curpats patcs =
assert(List.length curpats = List.length patcs);
- fold_left2 (fun acc ->
+ fold_left2 (fun acc ->
match acc with
| None -> find_split_pat | _ -> fun _ _ -> acc)
None curpats patcs
in find_split_pats curpats patcs
-
+
open Pp
open Termops
@@ -595,13 +595,13 @@ let pr_constr_pat env c =
| _ -> pr
let pr_pat env c =
- try
+ try
let patc = constr_of_pat env c in
try pr_constr_pat env patc with _ -> str"pr_constr_pat raised an exception"
with _ -> str"constr_of_pat raised an exception"
-
+
let pr_context env c =
- let pr_decl (id,b,_) =
+ let pr_decl (id,b,_) =
let bstr = match b with Some b -> str ":=" ++ spc () ++ print_constr_env env b | None -> mt() in
let idstr = match id with Name id -> pr_id id | Anonymous -> str"_" in
idstr ++ bstr
@@ -618,18 +618,18 @@ let pr_lhs env (delta, f, patcs) =
let pr_rhs env = function
| Empty var -> spc () ++ str ":=!" ++ spc () ++ print_constr_env env (mkRel var)
| Program rhs -> spc () ++ str ":=" ++ spc () ++ print_constr_env env rhs
-
+
let pr_clause env (lhs, rhs) =
- pr_lhs env lhs ++
+ pr_lhs env lhs ++
(let env' = push_rel_context (pi1 lhs) env in
pr_rhs env' rhs)
-
+
(* let pr_splitting env = function *)
(* | Compute cl -> str "Compute " ++ pr_clause env cl *)
(* | Split (lhs, n, indf, results, splits) -> *)
(* let pr_unification_result (ctx, n, c, pat, subst) = *)
-
+
(* unification_result array * splitting option array *)
let pr_clauses env =
@@ -637,36 +637,36 @@ let pr_clauses env =
let lhs_includes (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
pattern_includes patcs patcs'
-
+
let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
pattern_matches patcs patcs'
let rec split_on env var (delta, f, curpats as lhs) clauses =
let before, (id, _, ty), after = split_tele (pred var) delta in
- let unify, indf =
- match unify_type before ty with
+ let unify, indf =
+ match unify_type before ty with
| Some r -> r
| None -> assert false (* We decided... so it better be inductive *)
in
let clauses = ref clauses in
- let splits =
+ let splits =
Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) ->
match s with
| None -> None
- | Some s ->
+ | Some s ->
(* ctx' |- s cstr, s cstrpat *)
let newdelta =
- subst_context s (subst_rel_context 0 cstr
+ subst_context s (subst_rel_context 0 cstr
(lift_contextn ctxlen 1 after)) @ ctx' in
- let liftpats =
+ let liftpats =
(* delta |- curpats -> before; ctxc; id; after |- liftpats *)
- lift_pats ctxlen (succ var) curpats
+ lift_pats ctxlen (succ var) curpats
in
let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *)
lift_pat (pred var) 1 cstrpat
in
let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *)
- subst_pats env var liftpat liftpats
+ subst_pats env var liftpat liftpats
in
let lifts = (* before; ctxc |- s : newdelta ->
before; ctxc; after |- lifts : newdelta ; after *)
@@ -674,8 +674,8 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
in
let newpats = specialize_patterns lifts substpat in
let newlhs = (newdelta, f, newpats) in
- let matching, rest =
- fold_right (fun (lhs, rhs as clause) (matching, rest) ->
+ let matching, rest =
+ fold_right (fun (lhs, rhs as clause) (matching, rest) ->
if lhs_includes newlhs lhs then
(clause :: matching, rest)
else (matching, clause :: rest))
@@ -684,11 +684,11 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
clauses := rest;
if matching = [] then (
(* Try finding a splittable variable *)
- let (id, _) =
- fold_right (fun (id, _, ty as decl) (accid, ctx) ->
- match accid with
+ let (id, _) =
+ fold_right (fun (id, _, ty as decl) (accid, ctx) ->
+ match accid with
| Some _ -> (accid, ctx)
- | None ->
+ | None ->
match unify_type ctx ty with
| Some (unify, indf) ->
if array_for_all (fun (_, _, _, _, x) -> x = None) unify then
@@ -696,13 +696,13 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
else (None, decl :: ctx)
| None -> (None, decl :: ctx))
newdelta (None, [])
- in
+ in
match id with
| None ->
errorlabstrm "deppat"
(str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++
pr_lhs env newlhs)
- | Some id ->
+ | Some id ->
Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta))))
) else (
let splitting = make_split_aux env newlhs matching in
@@ -713,14 +713,14 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
(* errorlabstrm "deppat" *)
(* (str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); *)
Split (lhs, var, indf, unify, splits)
-
+
and make_split_aux env lhs clauses =
- let split =
- fold_left (fun acc (lhs', rhs) ->
- match acc with
+ let split =
+ fold_left (fun acc (lhs', rhs) ->
+ match acc with
| None -> find_split lhs lhs'
| _ -> acc) None clauses
- in
+ in
match split with
| Some var -> split_on env var lhs clauses
| None ->
@@ -742,7 +742,7 @@ and make_split_aux env lhs clauses =
let make_split env (f, delta, t) clauses =
make_split_aux env (delta, f, patvars_of_tele delta) clauses
-
+
open Evd
open Evarutil
@@ -755,18 +755,18 @@ let term_of_tree status isevar env (i, delta, ty) ann tree =
(* | Some (loc, i) -> *)
(* let (n, t) = lookup_rel_id i delta in *)
(* let t' = lift n t in *)
-
-
+
+
(* in *)
let rec aux = function
- | Compute ((ctx, _, pats as lhs), Program rhs) ->
+ | Compute ((ctx, _, pats as lhs), Program rhs) ->
let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in
mkCast(body, DEFAULTcast, typ), typ
| Compute ((ctx, _, pats as lhs), Empty split) ->
let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let split = (Name (id_of_string "split"),
+ let split = (Name (id_of_string "split"),
Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))),
Lazy.force Class_tactics.coq_nat)
in
@@ -774,25 +774,25 @@ let term_of_tree status isevar env (i, delta, ty) ann tree =
let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in
let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark (Define true)) let_ty' in
term, ty'
-
- | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) ->
+
+ | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) ->
let before, decl, after = split_tele (pred rel) ctx in
let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let branches =
- array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split ->
+ let branches =
+ array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split ->
match split with
| Some s -> aux s
- | None ->
+ | None ->
(* dead code, inversion will find a proof of False by splitting on the rel'th hyp *)
Class_tactics.coq_nat_of_int rel, Lazy.force Class_tactics.coq_nat)
- unif sp
+ unif sp
in
let branches_ctx =
Array.mapi (fun i (br, brt) -> (id_of_string ("m_" ^ string_of_int i), Some br, brt))
branches
in
- let n, branches_lets =
- Array.fold_left (fun (n, lets) (id, b, t) ->
+ let n, branches_lets =
+ Array.fold_left (fun (n, lets) (id, b, t) ->
(succ n, (Name id, Option.map (lift n) b, lift n t) :: lets))
(0, []) branches_ctx
in
@@ -800,18 +800,18 @@ let term_of_tree status isevar env (i, delta, ty) ann tree =
let case =
let ty = it_mkProd_or_LetIn ty' liftctx in
let ty = it_mkLambda_or_LetIn ty branches_lets in
- let nbbranches = (Name (id_of_string "branches"),
+ let nbbranches = (Name (id_of_string "branches"),
Some (Class_tactics.coq_nat_of_int (length branches_lets)),
Lazy.force Class_tactics.coq_nat)
in
- let nbdiscr = (Name (id_of_string "target"),
+ let nbdiscr = (Name (id_of_string "target"),
Some (Class_tactics.coq_nat_of_int (length before)),
Lazy.force Class_tactics.coq_nat)
in
let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in
let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark status) ty in
term
- in
+ in
let casetyp = it_mkProd_or_LetIn ty' ctx in
mkCast(case, DEFAULTcast, casetyp), casetyp
@@ -829,9 +829,9 @@ let locate_reference qid =
| SynDef kn -> true
let is_global id =
- try
+ try
locate_reference (qualid_of_ident id)
- with Not_found ->
+ with Not_found ->
false
let is_freevar ids env x =
@@ -841,12 +841,12 @@ let is_freevar ids env x =
try ignore(Environ.lookup_named x env) ; false
with _ -> not (is_global x)
with _ -> true
-
-let ids_of_patc c ?(bound=Idset.empty) l =
+
+let ids_of_patc c ?(bound=Idset.empty) l =
let found id bdvars l =
if not (is_freevar bdvars (Global.env ()) (snd id)) then l
- else if List.exists (fun (_, id') -> id' = snd id) l then l
- else id :: l
+ else if List.exists (fun (_, id') -> id' = snd id) l then l
+ else id :: l
in
let rec aux bdvars l c = match c with
| CRef (Ident lid) -> found lid bdvars l
@@ -858,11 +858,11 @@ let ids_of_patc c ?(bound=Idset.empty) l =
let interp_pats i isevar env impls pat sign recu =
let bound = Idset.singleton i in
let vars = ids_of_patc pat ~bound [] in
- let varsctx, env' =
+ let varsctx, env' =
fold_right (fun (loc, id) (ctx, env) ->
let decl =
let ty = e_new_evar isevar env ~src:(loc, BinderType (Name id)) (new_Type ()) in
- (Name id, None, ty)
+ (Name id, None, ty)
in
decl::ctx, push_rel decl env)
vars ([], env)
@@ -871,7 +871,7 @@ let interp_pats i isevar env impls pat sign recu =
let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in
let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in
match kind_of_term patt with
- | App (m, args) ->
+ | App (m, args) ->
if not (eq_constr m (mkRel (succ (length varsctx)))) then
user_err_loc (constr_loc pat, "interp_pats",
str "Expecting a pattern for " ++ pr_id i)
@@ -880,18 +880,18 @@ let interp_pats i isevar env impls pat sign recu =
str "Error parsing pattern: unnexpected left-hand side")
in
isevar := nf_evar_defs !isevar;
- (nf_rel_context_evar ( !isevar) varsctx,
+ (nf_rel_context_evar ( !isevar) varsctx,
nf_env_evar ( !isevar) env',
rev_map (nf_evar ( !isevar)) pats)
-
+
let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
let rhs' = match rhs with
- | Program p ->
+ | Program p ->
let ty = nf_isevar !isevar (substl patcs arity) in
Program (interp_casted_constr_evars isevar env' ~impls p ty)
| Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx))
- in ((ctx, i, pats_of_constrs (rev patcs)), rhs')
+ in ((ctx, i, pats_of_constrs (rev patcs)), rhs')
open Entries
@@ -905,10 +905,10 @@ let contrib_tactics_path =
let tactics_tac s =
make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)
-
-let equations_tac = lazy
- (Tacinterp.eval_tactic
- (TacArg(TacCall(dummy_loc,
+
+let equations_tac = lazy
+ (Tacinterp.eval_tactic
+ (TacArg(TacCall(dummy_loc,
ArgArg(dummy_loc, tactics_tac "equations"), []))))
let define_by_eqs with_comp i (l,ann) t nt eqs =
@@ -918,14 +918,14 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
let arity = interp_type_evars isevar env' t in
let sign = nf_rel_context_evar ( !isevar) sign in
let arity = nf_evar ( !isevar) arity in
- let arity =
+ let arity =
if with_comp then
let compid = add_suffix i "_comp" in
let ce =
{ const_entry_body = it_mkLambda_or_LetIn arity sign;
const_entry_type = None;
const_entry_opaque = false;
- const_entry_boxed = false}
+ const_entry_boxed = false}
in
let c =
Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition)
@@ -937,8 +937,8 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in
let fixdecls = [(Name i, None, ty)] in
let fixenv = push_rel_context fixdecls env in
- let equations =
- States.with_heavy_rollback (fun () ->
+ let equations =
+ States.with_heavy_rollback (fun () ->
Option.iter (Command.declare_interning_data data) nt;
map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
in
@@ -961,21 +961,21 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
let status = (* if is_recursive then Expand else *) Define false in
let t, ty = term_of_tree status isevar env' prob ann split in
let undef = undefined_evars !isevar in
- let t, ty = if is_recursive then
+ let t, ty = if is_recursive then
(it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls)
else t, ty
in
- let obls, t', ty' =
+ let obls, t', ty' =
Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
in
if is_recursive then
- ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
+ ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
~tactic:(Lazy.force equations_tac)
(Command.IsFixpoint [None, CStructRec]))
else
ignore(Subtac_obligations.add_definition
~implicits:impls i t' ty' ~tactic:(Lazy.force equations_tac) obls)
-
+
module Gram = Pcoq.Gram
module Vernac = Pcoq.Vernac_
module Tactic = Pcoq.Tactic
@@ -993,7 +993,7 @@ struct
end
open Rawterm
-open DeppatGram
+open DeppatGram
open Util
open Pcoq
open Prim
@@ -1002,7 +1002,7 @@ open G_vernac
GEXTEND Gram
GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
-
+
deppat_equations:
[ [ l = LIST1 equation SEP ";" -> l ] ]
;
@@ -1020,7 +1020,7 @@ GEXTEND Gram
|":="; c = Constr.lconstr -> Program c
] ]
;
-
+
END
type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type
@@ -1059,8 +1059,8 @@ VERNAC COMMAND EXTEND Define_equations2
decl_notation(nt) ] ->
[ equations false i l t nt eqs ]
END
-
-let rec int_of_coq_nat c =
+
+let rec int_of_coq_nat c =
match kind_of_term c with
| App (f, [| arg |]) -> succ (int_of_coq_nat arg)
| _ -> 0
@@ -1076,24 +1076,24 @@ let solve_equations_goal destruct_tac tac gl =
| _ -> error "Unnexpected goal")
| _ -> error "Unnexpected goal"
in
- let branches, b =
+ let branches, b =
let rec aux n c =
if n = 0 then [], c
else match kind_of_term c with
- | LetIn (Name id, br, brt, b) ->
+ | LetIn (Name id, br, brt, b) ->
let rest, b = aux (pred n) b in
(id, br, brt) :: rest, b
| _ -> error "Unnexpected goal"
in aux brs b
- in
+ in
let ids = targetn :: branchesn :: map pi1 branches in
let cleantac = tclTHEN (intros_using ids) (thin ids) in
let dotac = tclDO (succ targ) intro in
- let subtacs =
+ let subtacs =
tclTHENS destruct_tac
(map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br (Some brt) onConcl) tac) branches)
in tclTHENLIST [cleantac ; dotac ; subtacs] gl
-
+
TACTIC EXTEND solve_equations
[ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ]
END
@@ -1110,7 +1110,7 @@ let specialize_hyp id gl =
let evars = ref (create_evar_defs (project gl)) in
let rec aux in_eqs acc ty =
match kind_of_term ty with
- | Prod (_, t, b) ->
+ | Prod (_, t, b) ->
(match kind_of_term t with
| App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
let pt = mkApp (Lazy.force coq_eq, [| eqty; x; x |]) in
@@ -1124,14 +1124,14 @@ let specialize_hyp id gl =
if e_conv env evars pt t then
aux true (mkApp (acc, [| p |])) (subst1 p b)
else error "Unconvertible members of an heterogeneous equality"
- | _ ->
+ | _ ->
if in_eqs then acc, in_eqs, ty
- else
+ else
let e = e_new_evar evars env t in
aux false (mkApp (acc, [| e |])) (subst1 e b))
| t -> acc, in_eqs, ty
- in
- try
+ in
+ try
let acc, worked, ty = aux false (mkVar id) ty in
let ty = Evarutil.nf_isevar !evars ty in
if worked then
@@ -1140,9 +1140,9 @@ let specialize_hyp id gl =
(exact_no_check (Evarutil.nf_isevar !evars acc)) gl
else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
with e -> tclFAIL 0 (Cerrors.explain_exn e) gl
-
+
TACTIC EXTEND specialize_hyp
-[ "specialize_hypothesis" constr(c) ] -> [
+[ "specialize_hypothesis" constr(c) ] -> [
match kind_of_term c with
| Var id -> specialize_hyp id
| _ -> tclFAIL 0 (str "Not an hypothesis") ]
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index d65b520b65..3c947e29cf 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -16,11 +16,11 @@ open Util
open Subtac_utils
open Proof_type
-let trace s =
+let trace s =
if !Flags.debug then (msgnl s; msgerr s)
else ()
-let succfix (depth, fixrels) =
+let succfix (depth, fixrels) =
(succ depth, List.map succ fixrels)
type oblinfo =
@@ -32,41 +32,41 @@ type oblinfo =
ev_typ: types;
ev_tac: Tacexpr.raw_tactic_expr option;
ev_deps: Intset.t }
-
-(** Substitute evar references in t using De Bruijn indices,
+
+(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
-let subst_evar_constr evs n t =
+let subst_evar_constr evs n t =
let seen = ref Intset.empty in
let transparent = ref Idset.empty in
let evar_info id = List.assoc id evs in
let rec substrec (depth, fixrels) c = match kind_of_term c with
| Evar (k, args) ->
- let { ev_name = (id, idstr) ;
+ let { ev_name = (id, idstr) ;
ev_hyps = hyps ; ev_chop = chop } =
try evar_info k
- with Not_found ->
+ with Not_found ->
anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
in
seen := Intset.add id !seen;
- (* Evar arguments are created in inverse order,
+ (* Evar arguments are created in inverse order,
and we must not apply to defined ones (i.e. LetIn's)
*)
- let args =
- let n = match chop with None -> 0 | Some c -> c in
+ let args =
+ let n = match chop with None -> 0 | Some c -> c in
let (l, r) = list_chop n (List.rev (Array.to_list args)) in
List.rev r
in
let args =
let rec aux hyps args acc =
match hyps, args with
- ((_, None, _) :: tlh), (c :: tla) ->
+ ((_, None, _) :: tlh), (c :: tla) ->
aux tlh tla ((substrec (depth, fixrels) c) :: acc)
| ((_, Some _, _) :: tlh), (_ :: tla) ->
aux tlh tla acc
| [], [] -> acc
| _, _ -> acc (*failwith "subst_evars: invalid argument"*)
- in aux hyps args []
+ in aux hyps args []
in
if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
transparent := Idset.add idstr !transparent;
@@ -74,25 +74,25 @@ let subst_evar_constr evs n t =
| Fix _ ->
map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
| _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
- in
+ in
let t' = substrec (0, []) t in
t', !seen, !transparent
-
-(** Substitute variable references in t using De Bruijn indices,
+
+(** Substitute variable references in t using De Bruijn indices,
where n binders were passed through. *)
-let subst_vars acc n t =
+let subst_vars acc n t =
let var_index id = Util.list_index id acc in
let rec substrec depth c = match kind_of_term c with
| Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
| _ -> map_constr_with_binders succ substrec depth c
- in
+ in
substrec 0 t
(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
to a product : forall H1 : t1, ..., forall Hn : tn, concl.
Changes evars and hypothesis references to variable references.
-*)
+*)
let etype_of_evar evs hyps concl =
let rec aux acc n = function
(id, copt, t) :: tl ->
@@ -102,13 +102,13 @@ let etype_of_evar evs hyps concl =
let s' = Intset.union s s' in
let trans' = Idset.union trans trans' in
(match copt with
- Some c ->
+ Some c ->
let c', s'', trans'' = subst_evar_constr evs n c in
let c' = subst_vars acc 0 c' in
- mkNamedProd_or_LetIn (id, Some c', t'') rest,
- Intset.union s'' s',
+ mkNamedProd_or_LetIn (id, Some c', t'') rest,
+ Intset.union s'' s',
Idset.union trans'' trans'
- | None ->
+ | None ->
mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
| [] ->
let t', s, trans = subst_evar_constr evs n concl in
@@ -117,25 +117,25 @@ let etype_of_evar evs hyps concl =
open Tacticals
-
-let trunc_named_context n ctx =
+
+let trunc_named_context n ctx =
let len = List.length ctx in
list_firstn (len - n) ctx
-
-let rec chop_product n t =
+
+let rec chop_product n t =
if n = 0 then Some t
- else
+ else
match kind_of_term t with
| Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
| _ -> None
let evar_dependencies evm ev =
- let one_step deps =
- Intset.fold (fun ev s ->
+ let one_step deps =
+ Intset.fold (fun ev s ->
let evi = Evd.find evm ev in
Intset.union (Evarutil.evars_of_evar_info evi) s)
deps deps
- in
+ in
let rec aux deps =
let deps' = one_step deps in
if Intset.equal deps deps' then deps
@@ -143,13 +143,13 @@ let evar_dependencies evm ev =
in aux (Intset.singleton ev)
let sort_dependencies evl =
- List.sort (fun (_, _, deps) (_, _, deps') ->
+ List.sort (fun (_, _, deps) (_, _, deps') ->
if Intset.subset deps deps' then (* deps' depends on deps *) -1
else if Intset.subset deps' deps then 1
else Intset.compare deps deps')
evl
-
-let eterm_obligations env name isevars evm fs ?status t ty =
+
+let eterm_obligations env name isevars evm fs ?status t ty =
(* 'Serialize' the evars *)
let nc = Environ.named_context env in
let nc_len = Sign.named_context_length nc in
@@ -157,37 +157,37 @@ let eterm_obligations env name isevars evm fs ?status t ty =
let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
let sevl = sort_dependencies evl in
let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
- let evn =
+ let evn =
let i = ref (-1) in
- List.rev_map (fun (id, ev) -> incr i;
+ List.rev_map (fun (id, ev) -> incr i;
(id, (!i, id_of_string
(string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
ev)) evl
in
- let evts =
+ let evts =
(* Remove existential variables in types and build the corresponding products *)
- fold_right
+ fold_right
(fun (id, (n, nstr), ev) l ->
let hyps = Evd.evar_filtered_context ev in
let hyps = trunc_named_context nc_len hyps in
let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
- let evtyp, hyps, chop =
+ let evtyp, hyps, chop =
match chop_product fs evtyp with
| Some t -> t, trunc_named_context fs hyps, fs
| None -> evtyp, hyps, 0
in
let loc, k = evar_source id isevars in
let status = match k with QuestionMark o -> Some o | _ -> status in
- let status, chop = match status with
+ let status, chop = match status with
| Some (Define true as stat) ->
- if chop <> fs then Define false, None
+ if chop <> fs then Define false, None
else stat, Some chop
| Some s -> s, None
| None -> Define true, None
in
- let tac = match ev.evar_extra with
- | Some t ->
- if Dyn.tag t = "tactic" then
+ let tac = match ev.evar_extra with
+ | Some t ->
+ if Dyn.tag t = "tactic" then
Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
else None
| None -> None
@@ -195,14 +195,14 @@ let eterm_obligations env name isevars evm fs ?status t ty =
let info = { ev_name = (n, nstr);
ev_hyps = hyps; ev_status = status; ev_chop = chop;
ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
- in (id, info) :: l)
+ in (id, info) :: l)
evn []
- in
+ in
let t', _, transparent = (* Substitute evar refs in the term by variables *)
- subst_evar_constr evts 0 t
+ subst_evar_constr evts 0 t
in
let ty, _, _ = subst_evar_constr evts 0 ty in
- let evars =
+ let evars =
List.map (fun (_, info) ->
let { ev_name = (_, name); ev_status = status;
ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 413823ffe9..1d1c512662 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -19,12 +19,12 @@ val mkMetas : int -> constr list
val evar_dependencies : evar_map -> int -> Intset.t
val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
-
+
(* env, id, evars, number of function prototypes to try to clear from
evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
- ?status:obligation_definition_status -> constr -> types ->
- (identifier * types * loc * obligation_definition_status * Intset.t *
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
+ ?status:obligation_definition_status -> constr -> types ->
+ (identifier * types * loc * obligation_definition_status * Intset.t *
Tacexpr.raw_tactic_expr option) array * constr * types
(* Obl. name, type as product, location of the original evar, associated tactic,
status and dependencies as indexes into the array *)
diff --git a/plugins/subtac/g_eterm.ml4 b/plugins/subtac/g_eterm.ml4
index 095e5fafc9..53ce5b8d64 100644
--- a/plugins/subtac/g_eterm.ml4
+++ b/plugins/subtac/g_eterm.ml4
@@ -20,7 +20,7 @@
open Eterm
TACTIC EXTEND eterm
- [ "eterm" ] -> [
+ [ "eterm" ] -> [
(fun gl ->
let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in
Eterm.etermtac (evm, t) gl) ]
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index a1cbeb710a..098418a7e3 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -7,7 +7,7 @@
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
(*
@@ -45,7 +45,7 @@ struct
end
open Rawterm
-open SubtacGram
+open SubtacGram
open Util
open Pcoq
open Prim
@@ -54,14 +54,14 @@ let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Spec
GEXTEND Gram
GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt;
-
+
subtac_gallina_loc:
[ [ g = Vernac.gallina -> loc, g
| g = Vernac.gallina_ext -> loc, g ] ]
;
subtac_nameopt:
- [ [ "ofb"; id=Prim.ident -> Some (id)
+ [ [ "ofb"; id=Prim.ident -> Some (id)
| -> None ] ]
;
@@ -115,42 +115,42 @@ let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e
VERNAC COMMAND EXTEND Subtac_Obligations
| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ subtac_obligation (num, Some name, Some t) ]
| [ "Obligation" integer(num) "of" ident(name) ] -> [ subtac_obligation (num, Some name, None) ]
-| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ subtac_obligation (num, None, Some t) ]
+| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ subtac_obligation (num, None, Some t) ]
| [ "Obligation" integer(num) ] -> [ subtac_obligation (num, None, None) ]
| [ "Next" "Obligation" "of" ident(name) ] -> [ next_obligation (Some name) ]
| [ "Next" "Obligation" ] -> [ next_obligation None ]
END
VERNAC COMMAND EXTEND Subtac_Solve_Obligation
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] ->
+| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] ->
[ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] ->
+| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] ->
[ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
END
VERNAC COMMAND EXTEND Subtac_Solve_Obligations
-| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] ->
+| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] ->
[ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligations" "using" tactic(t) ] ->
+| [ "Solve" "Obligations" "using" tactic(t) ] ->
[ try_solve_obligations None (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligations" ] ->
+| [ "Solve" "Obligations" ] ->
[ try_solve_obligations None None ]
END
VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
-| [ "Solve" "All" "Obligations" "using" tactic(t) ] ->
+| [ "Solve" "All" "Obligations" "using" tactic(t) ] ->
[ solve_all_obligations (Some (Tacinterp.interp t)) ]
-| [ "Solve" "All" "Obligations" ] ->
+| [ "Solve" "All" "Obligations" ] ->
[ solve_all_obligations None ]
END
VERNAC COMMAND EXTEND Subtac_Admit_Obligations
-| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
-| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
+| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
END
VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ]
END
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index b5e2880134..56134d7086 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -23,7 +23,7 @@ open Typeops
open Libnames
open Classops
open List
-open Recordops
+open Recordops
open Evarutil
open Pretype_errors
open Rawterm
@@ -50,14 +50,14 @@ open Tacinterp
open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
- if not (evm = Evd.empty) then
+ if not (evm = Evd.empty) then
let stmt_id = Nameops.add_suffix id "_stmt" in
let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
match Subtac_obligations.add_definition stmt_id c' typ obls with
- | Subtac_obligations.Defined cst -> constant_value (Global.env())
+ | Subtac_obligations.Defined cst -> constant_value (Global.env())
(match cst with ConstRef kn -> kn | _ -> assert false)
- | _ ->
- errorlabstrm "start_proof"
+ | _ ->
+ errorlabstrm "start_proof"
(str "The statement obligations could not be resolved automatically, " ++ spc () ++
str "write a statement definition first.")
else
@@ -75,30 +75,30 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
next_global_ident_away false (id_of_string "Unnamed_thm")
(Pfedit.get_all_proof_names ())
in
- let evm, c, typ, imps =
- Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
+ let evm, c, typ, imps =
+ Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
- Command.start_proof id kind c (fun loc gr ->
+ Command.start_proof id kind c (fun loc gr ->
Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
hook loc gr)
-
+
let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
-
+
let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
-
+
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
let declare_assumption env isevars idl is_coe k bl c nl =
if not (Pfedit.refining ()) then
let id = snd (List.hd idl) in
- let evm, c, typ, imps =
- Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
+ let evm, c, typ, imps =
+ Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
List.iter (Command.declare_one_assumption is_coe k c imps false nl) idl
@@ -115,9 +115,9 @@ let dump_variable lid = ()
let vernac_assumption env isevars kind l nl =
let global = fst kind = Global in
- List.iter (fun (is_coe,(idl,c)) ->
+ List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
- List.iter (fun lid ->
+ List.iter (fun lid ->
if global then Dumpglob.dump_definition lid (not global) "ax"
else dump_variable lid) idl;
declare_assumption env isevars idl is_coe kind [] c nl) l
@@ -125,7 +125,7 @@ let vernac_assumption env isevars kind l nl =
let check_fresh (loc,id) =
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
user_err_loc (loc,"",pr_id id ++ str " already exists")
-
+
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
@@ -133,25 +133,25 @@ let subtac (loc, command) =
let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
- | VernacDefinition (defkind, (_, id as lid), expr, hook) ->
+ | VernacDefinition (defkind, (_, id as lid), expr, hook) ->
check_fresh lid;
Dumpglob.dump_definition lid false "def";
(match expr with
- | ProveBody (bl, t) ->
+ | ProveBody (bl, t) ->
if Lib.is_modtype () then
errorlabstrm "Subtac_command.StartProof"
(str "Proof editing mode not supported in module types");
- start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
+ start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
- | DefineBody (bl, _, c, tycon) ->
+ | DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
- | VernacFixpoint (l, b) ->
- List.iter (fun ((lid, _, _, _, _), _) ->
+ | VernacFixpoint (l, b) ->
+ List.iter (fun ((lid, _, _, _, _), _) ->
check_fresh lid;
Dumpglob.dump_definition lid false "fix") l;
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
-
+
| VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
Dumpglob.dump_definition id false "prf";
if not(Pfedit.refining ()) then
@@ -163,30 +163,30 @@ let subtac (loc, command) =
(str "Proof editing mode not supported in module types");
check_fresh id;
start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
-
- | VernacAssumption (stre,nl,l) ->
+
+ | VernacAssumption (stre,nl,l) ->
vernac_assumption env isevars stre l nl
-
+
| VernacInstance (glob, sup, is, props, pri) ->
dump_constraint "inst" is;
ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
-
+
| VernacCoFixpoint (l, b) ->
- if Dumpglob.dump () then
+ if Dumpglob.dump () then
List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
ignore(Subtac_command.build_corecursive l b)
-
- (*| VernacEndProof e ->
+
+ (*| VernacEndProof e ->
subtac_end_proof e*)
| _ -> user_err_loc (loc,"", str ("Invalid Program command"))
- with
+ with
| Typing_error e ->
msg_warning (str "Type error in Program tactic:");
- let cmds =
+ let cmds =
(match e with
| NonFunctionalApp (loc, x, mux, e) ->
- str "non functional application of term " ++
+ str "non functional application of term " ++
e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
| NonSigma (loc, t) ->
str "Term is not of Sigma type: " ++ t
@@ -197,10 +197,10 @@ let subtac (loc, command) =
str "Term is ill-sorted:" ++ spc () ++ t
)
in msg_warning cmds
-
+
| Subtyping_error e ->
msg_warning (str "(Program tactic) Subtyping error:");
- let cmds =
+ let cmds =
match e with
| UncoercibleInferType (loc, x, y) ->
str "Uncoercible terms:" ++ spc ()
@@ -217,15 +217,15 @@ let subtac (loc, command) =
| Cases.PatternMatchingError (env, exn) as e ->
debug 2 (Himsg.explain_pattern_matching_error env exn);
raise e
-
+
| Type_errors.TypeError (env, exn) as e ->
debug 2 (Himsg.explain_type_error env exn);
raise e
-
+
| Pretype_errors.PretypeError (env, exn) as e ->
debug 2 (Himsg.explain_pretype_error env exn);
raise e
-
+
| (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
Stdpp.Exc_located (loc, e') as e) ->
debug 2 (str "Parsing exception: ");
@@ -233,14 +233,14 @@ let subtac (loc, command) =
| Type_errors.TypeError (env, exn) ->
debug 2 (Himsg.explain_type_error env exn);
raise e
-
+
| Pretype_errors.PretypeError (env, exn) ->
debug 2 (Himsg.explain_pretype_error env exn);
raise e
| e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
raise e)
-
- | e ->
+
+ | e ->
msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
raise e
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 5f2cb601be..d54bbee4e3 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -45,7 +45,7 @@ let mssg_may_need_inversion () =
(* Utils *)
let make_anonymous_patvars =
- list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous))
+ list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous))
(* Environment management *)
let push_rels vars env = List.fold_right push_rel vars env
@@ -72,7 +72,7 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
| NonDepAlias ->
if (not (dependent (mkRel 1) j.uj_type))
or (* A leaf: *) isRel deppat
- then
+ then
(* The body of pat is not needed to type j - see *)
(* insert_aliases - and both deppat and nondeppat have the *)
(* same type, then one can freely substitute one by the other *)
@@ -94,7 +94,7 @@ type rhs =
}
type equation =
- { patterns : cases_pattern list;
+ { patterns : cases_pattern list;
rhs : rhs;
alias_stack : name list;
eqn_loc : loc;
@@ -154,7 +154,7 @@ let feed_history arg = function
Continuation (n-1, arg :: l, h)
| Continuation (n, _, _) ->
anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
- | Result _ ->
+ | Result _ ->
anomaly "Exhausted pattern history"
(* This is for non exhaustive error message *)
@@ -185,7 +185,7 @@ let rec simplify_history = function
let pat = match f with
| AliasConstructor pci ->
PatCstr (dummy_loc,pci,pargs,Anonymous)
- | AliasLeaf ->
+ | AliasLeaf ->
assert (l = []);
PatVar (dummy_loc, Anonymous) in
feed_history pat rh
@@ -203,7 +203,7 @@ let push_history_pattern n current cont =
where tomatch is some sequence of "instructions" (t1 ... tn)
- and mat is some matrix
+ and mat is some matrix
(p11 ... p1n -> rhs1)
( ... )
(pm1 ... pmn -> rhsm)
@@ -263,7 +263,7 @@ let rec find_row_ind = function
let inductive_template isevars env tmloc ind =
let arsign = get_full_arity_sign env ind in
- let hole_source = match tmloc with
+ let hole_source = match tmloc with
| Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
| None -> fun _ -> (dummy_loc, Evd.InternalHole) in
let (_,evarl,_) =
@@ -273,7 +273,7 @@ let inductive_template isevars env tmloc ind =
| None ->
let ty' = substl subst ty in
let e = e_new_evar isevars env ~src:(hole_source n) ty' in
- (e::subst,e::evarl,n+1)
+ (e::subst,e::evarl,n+1)
| Some b ->
(b::subst,evarl,n+1))
arsign ([],[],1) in
@@ -293,7 +293,7 @@ let evd_comb2 f isevars x y =
let context_of_arsign l =
let (x, _) = List.fold_right
- (fun c (x, n) ->
+ (fun c (x, n) ->
(lift_rel_context n c @ x, List.length c + n))
l ([], 0)
in x
@@ -302,11 +302,11 @@ let context_of_arsign l =
let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
- let subst, len =
+ let subst, len =
List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
let signlen = List.length sign in
match kind_of_term tm with
- | Rel n when dependent tm c
+ | Rel n when dependent tm c
&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
((n, len) :: subst, len - signlen)
| Rel n when signlen > 1 (* The term is of a dependent type,
@@ -314,12 +314,12 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
(match tmtype with
| NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
| IsInd (_, IndType(indf,realargs)) ->
- let subst =
- if dependent tm c && List.for_all isRel realargs
- then (n, 1) :: subst else subst
+ let subst =
+ if dependent tm c && List.for_all isRel realargs
+ then (n, 1) :: subst else subst
in
List.fold_left
- (fun (subst, len) arg ->
+ (fun (subst, len) arg ->
match kind_of_term arg with
| Rel n when dependent arg c ->
((n, len) :: subst, pred len)
@@ -330,18 +330,18 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
in
let rec predicate lift c =
match kind_of_term c with
- | Rel n when n > lift ->
- (try
+ | Rel n when n > lift ->
+ (try
(* Make the predicate dependent on the matched variable *)
let idx = List.assoc (n - lift) subst in
mkRel (idx + lift)
- with Not_found ->
+ with Not_found ->
(* A variable that is not matched, lift over the arsign. *)
mkRel (n + nar))
| _ ->
- map_constr_with_binders succ predicate lift c
+ map_constr_with_binders succ predicate lift c
in
- try
+ try
(* The tycon may be ill-typed after abstraction. *)
let pred = predicate 0 c in
let env' = push_rel_context (context_of_arsign arsign) env in
@@ -352,7 +352,7 @@ module Cases_F(Coercion : Coercion.S) : S = struct
let inh_coerce_to_ind isevars env ty tyi =
let expected_typ = inductive_template isevars env None tyi in
- (* devrait être indifférent d'exiger leq ou pas puisque pour
+ (* devrait être indifférent d'exiger leq ou pas puisque pour
un inductif cela doit être égal *)
let _ = e_cumul env isevars expected_typ ty in ()
@@ -395,7 +395,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
(* Ideally, we could find a common inductive type to which both the
term to match and the patterns coerce *)
(* In practice, we coerce the term to match if it is not already an
- inductive type and it is not dependent; moreover, we use only
+ inductive type and it is not dependent; moreover, we use only
the first pattern type and forget about the others *)
let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
let typ =
@@ -479,7 +479,7 @@ let rec adjust_local_defs loc = function
| [], [] -> []
| _ -> raise NotAdjustable
-let check_and_adjust_constructor env ind cstrs = function
+let check_and_adjust_constructor env ind cstrs = function
| PatVar _ as pat -> pat
| PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
(* Check it is constructor of the right type *)
@@ -490,7 +490,7 @@ let check_and_adjust_constructor env ind cstrs = function
let nb_args_constr = ci.cs_nargs in
if List.length args = nb_args_constr then pat
else
- try
+ try
let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
in PatCstr (loc, cstr, args', alias)
with NotAdjustable ->
@@ -500,7 +500,7 @@ let check_and_adjust_constructor env ind cstrs = function
(* Try to insert a coercion *)
try
Coercion.inh_pattern_coerce_to loc pat ind' ind
- with Not_found ->
+ with Not_found ->
error_bad_constructor_loc loc cstr ind
let check_all_variables typ mat =
@@ -512,14 +512,14 @@ let check_all_variables typ mat =
mat
let check_unused_pattern env eqn =
- if not !(eqn.used) then
+ if not !(eqn.used) then
raise_pattern_matching_error
(eqn.eqn_loc, env, UnusedClause eqn.patterns)
let set_used_pattern eqn = eqn.used := true
let extract_rhs pb =
- match pb.mat with
+ match pb.mat with
| [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
| eqn::_ ->
set_used_pattern eqn;
@@ -558,7 +558,7 @@ let dependent_decl a = function
let rec find_dependency_list k n = function
| [] -> []
- | (used,tdeps,d)::rest ->
+ | (used,tdeps,d)::rest ->
let deps = find_dependency_list k (n+1) rest in
if used && dependent_decl (mkRel n) d
then list_add_set (List.length rest + 1) (list_union deps tdeps)
@@ -579,7 +579,7 @@ let find_dependencies_signature deps_in_rhs typs =
(* A Pushed term to match has just been substituted by some
constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
- match
+ match
- all terms to match and to push (dependent on t by definition)
must have (Rel depth) substituted by t and Rel's>depth lifted by n
@@ -604,7 +604,7 @@ let regeneralize_index_tomatch n =
::(genrec (depth+1) rest) in
genrec 0
-let rec replace_term n c k t =
+let rec replace_term n c k t =
if t = mkRel (n+k) then lift k c
else map_constr_with_binders succ (replace_term n c) k t
@@ -652,7 +652,7 @@ let lift_tomatch_stack n = liftn_tomatch_stack n 1
[match y with (S (S x)) => x | x => x end] should be compiled into
[match y with O => y | (S n) => match n with O => y | (S x) => x end end]
- and [match y with (S (S n)) => n | n => n end] into
+ and [match y with (S (S n)) => n | n => n end] into
[match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end]
i.e. user names should be preserved and created names should not
@@ -667,7 +667,7 @@ let merge_names get_name = List.map2 (merge_name get_name)
let get_names env sign eqns =
let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in
(* If any, we prefer names used in pats, from top to bottom *)
- let names2 =
+ let names2 =
List.fold_right
(fun (pats,eqn) names -> merge_names alias_of_pat pats names)
eqns names1 in
@@ -681,7 +681,7 @@ let get_names env sign eqns =
let na =
merge_name
(fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid))
- d na
+ d na
in
(na::l,(out_name na)::avoid))
([],allvars) (List.rev sign) names2 in
@@ -722,7 +722,7 @@ let build_aliases_context env sigma names allpats pats =
let oldallpats = List.map List.tl oldallpats in
let decl = (na,Some deppat,t) in
let a = (deppat,nondeppat,d,t) in
- insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1)
+ insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1)
newallpats oldallpats (pats,names)
| [], [] -> newallpats, sign1, sign2, env
| _ -> anomaly "Inconsistent alias and name lists" in
@@ -732,7 +732,7 @@ let build_aliases_context env sigma names allpats pats =
let insert_aliases_eqn sign eqnnames alias_rest eqn =
let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in
push_rels_eqn thissign { eqn with alias_stack = alias_rest; }
-
+
let insert_aliases env sigma alias eqns =
(* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
@@ -741,7 +741,7 @@ let insert_aliases env sigma alias eqns =
let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
(* names2 takes the meet of all needed aliases *)
- let names2 =
+ let names2 =
List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in
(* Only needed aliases are kept by build_aliases_context *)
let eqnsnames, sign1, sign2, env =
@@ -753,12 +753,12 @@ let insert_aliases env sigma alias eqns =
(* Functions to deal with elimination predicate *)
exception Occur
-let noccur_between_without_evar n m term =
+let noccur_between_without_evar n m term =
let rec occur_rec n c = match kind_of_term c with
| Rel p -> if n<=p && p<n+m then raise Occur
| Evar (_,cl) -> ()
| _ -> iter_constr_with_binders succ occur_rec n c
- in
+ in
try occur_rec n term; true with Occur -> false
(* Inferring the predicate *)
@@ -836,7 +836,7 @@ let rec transpose_args n =
let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
-let reloc_operator (k,n) = function OpRel p when p > k ->
+let reloc_operator (k,n) = function OpRel p when p > k ->
let rec unify_clauses k pv =
let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in
let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
@@ -894,7 +894,7 @@ let infer_predicate loc env isevars typs cstrs indf =
*)
(* "TODO4-2" *)
(* We skip parameters *)
- let cis =
+ let cis =
Array.map
(fun cs ->
applist (mkConstruct cs.cs_cstr, extended_rel_list 0 cs.cs_args))
@@ -1122,8 +1122,8 @@ let group_equations pb ind current cstrs mat =
(fun eqn () ->
let rest = remove_current_pattern eqn in
let pat = current_pattern eqn in
- match check_and_adjust_constructor pb.env ind cstrs pat with
- | PatVar (_,name) ->
+ match check_and_adjust_constructor pb.env ind cstrs pat with
+ | PatVar (_,name) ->
(* This is a default clause that we expand *)
for i=1 to Array.length cstrs do
let n = cstrs.(i-1).cs_nargs in
@@ -1176,10 +1176,10 @@ let build_branch current deps pb eqns const_info =
& not (known_dependent pb.pred) & deps = []
then
NonDepAlias
- else
+ else
DepAlias
in
- let history =
+ let history =
push_history_pattern const_info.cs_nargs
(AliasConstructor const_info.cs_cstr)
pb.history in
@@ -1204,7 +1204,7 @@ let build_branch current deps pb eqns const_info =
find_dependencies_signature
(dependencies_in_rhs const_info.cs_nargs eqns) (List.rev typs) in
- (* The dependent term to subst in the types of the remaining UnPushed
+ (* The dependent term to subst in the types of the remaining UnPushed
terms is relative to the current context enriched by topushs *)
let ci = build_dependent_constructor const_info in
@@ -1283,7 +1283,7 @@ and match_current pb tomatch =
let brvals = Array.map (fun (v,_) -> v) brs in
let brtyps = Array.map (fun (_,t) -> t) brs in
let (pred,typ,s) =
- find_predicate pb.caseloc pb.env pb.isevars
+ find_predicate pb.caseloc pb.env pb.isevars
pb.pred brtyps cstrs current indt pb.tomatch in
let ci = make_case_info pb.env mind pb.casestyle in
let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
@@ -1382,10 +1382,10 @@ let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
e_new_evar isevars env ~src:(loc, Evd.CasesType)
(Retyping.get_type_of env ( !isevars) c)
else
- map_constr_with_full_binders push_rel build_skeleton env c
+ map_constr_with_full_binders push_rel build_skeleton env c
in
names, build_skeleton env (lift n c)
-
+
(* Here, [pred] is assumed to be in the context built from all *)
(* realargs and terms to match *)
let build_initial_predicate isdep allnames pred =
@@ -1396,7 +1396,7 @@ let build_initial_predicate isdep allnames pred =
let names' = if isdep then List.tl names else names in
let n' = n + List.length names' in
let pred, p, user_p =
- if isdep then
+ if isdep then
if dependent (mkRel (nar-n')) pred then pred, 1, 1
else liftn (-1) (nar-n') pred, 0, 1
else pred, 0, 0 in
@@ -1414,10 +1414,10 @@ let build_initial_predicate isdep allnames pred =
let extract_arity_signature env0 tomatchl tmsign =
let get_one_sign n tm (na,t) =
match tm with
- | NotInd (bo,typ) ->
+ | NotInd (bo,typ) ->
(match t with
| None -> [na,Option.map (lift n) bo,lift n typ]
- | Some (loc,_,_,_) ->
+ | Some (loc,_,_,_) ->
user_err_loc (loc,"",
str "Unexpected type annotation for a term of non inductive type"))
| IsInd (_,IndType(indf,realargs)) ->
@@ -1448,10 +1448,10 @@ let extract_arity_signature env0 tomatchl tmsign =
let extract_arity_signatures env0 tomatchl tmsign =
let get_one_sign tm (na,t) =
match tm with
- | NotInd (bo,typ) ->
+ | NotInd (bo,typ) ->
(match t with
| None -> [na,bo,typ]
- | Some (loc,_,_,_) ->
+ | Some (loc,_,_,_) ->
user_err_loc (loc,"",
str "Unexpected type annotation for a term of non inductive type"))
| IsInd (_,IndType(indf,realargs)) ->
@@ -1487,19 +1487,19 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon =
| None -> j
let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false)
-
-let string_of_name name =
+
+let string_of_name name =
match name with
| Anonymous -> "anonymous"
| Name n -> string_of_id n
-
+
let id_of_name n = id_of_string (string_of_name n)
-let make_prime_id name =
+let make_prime_id name =
let str = string_of_name name in
id_of_string str, id_of_string (str ^ "'")
-let prime avoid name =
+let prime avoid name =
let previd, id = make_prime_id name in
previd, next_ident_away_from id avoid
@@ -1508,28 +1508,28 @@ let make_prime avoid prevname =
avoid := id :: !avoid;
previd, id
-let eq_id avoid id =
+let eq_id avoid id =
let hid = id_of_string ("Heq_" ^ string_of_id id) in
let hid' = next_ident_away_from hid avoid in
hid'
let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y =
+let mk_JMeq typ x typ' y =
mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
-
+
let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
-let constr_of_pat env isevars arsign pat avoid =
- let rec typ env (ty, realargs) pat avoid =
+let constr_of_pat env isevars arsign pat avoid =
+ let rec typ env (ty, realargs) pat avoid =
match pat with
- | PatVar (l,name) ->
+ | PatVar (l,name) ->
let name, avoid = match name with
Name n -> name, avoid
- | Anonymous ->
+ | Anonymous ->
let previd, id = prime avoid (Name (id_of_string "wildcard")) in
- Name id, id :: avoid
+ Name id, id :: avoid
in
PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
| PatCstr (l,((_, i) as cstr),args,alias) ->
@@ -1541,11 +1541,11 @@ let constr_of_pat env isevars arsign pat avoid =
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
assert(nb_args_constr = List.length args);
- let patargs, args, sign, env, n, m, avoid =
+ let patargs, args, sign, env, n, m, avoid =
List.fold_right2
(fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) ->
- let pat', sign', arg', typ', argtypargs, n', avoid =
- typ env (lift (n - m) t, []) ua avoid
+ let pat', sign', arg', typ', argtypargs, n', avoid =
+ typ env (lift (n - m) t, []) ua avoid
in
let args' = arg' :: List.map (lift n') args in
let env' = push_rels sign' env in
@@ -1558,7 +1558,7 @@ let constr_of_pat env isevars arsign pat avoid =
let cstr = mkConstruct ci.cs_cstr in
let app = applistc cstr (List.map (lift (List.length sign)) params) in
let app = applistc app args in
- let apptype = Retyping.get_type_of env ( !isevars) app in
+ let apptype = Retyping.get_type_of env ( !isevars) app in
let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in
match alias with
Anonymous ->
@@ -1573,38 +1573,38 @@ let constr_of_pat env isevars arsign pat avoid =
let eq_t = mk_eq (lift (succ m) ty)
(mkRel 1) (* alias *)
(lift 1 app) (* aliased term *)
- in
+ in
let neq = eq_id avoid id in
(Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid
with Reduction.NotConvertible -> sign, 1, avoid
in
(* Mark the equality as a hole *)
pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
- in
- let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in
+ in
+ let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in
pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid
(* shadows functional version *)
-let eq_id avoid id =
+let eq_id avoid id =
let hid = id_of_string ("Heq_" ^ string_of_id id) in
let hid' = next_ident_away_from hid !avoid in
avoid := hid' :: !avoid;
hid'
-let rels_of_patsign =
- List.map (fun ((na, b, t) as x) ->
- match b with
+let rels_of_patsign =
+ List.map (fun ((na, b, t) as x) ->
+ match b with
| Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
| _ -> x)
-let vars_of_ctx ctx =
+let vars_of_ctx ctx =
let _, y =
- List.fold_right (fun (na, b, t) (prev, vars) ->
- match b with
- | Some t' when kind_of_term t' = Rel 0 ->
- prev,
- (RApp (dummy_loc,
+ List.fold_right (fun (na, b, t) (prev, vars) ->
+ match b with
+ | Some t' when kind_of_term t' = Rel 0 ->
+ prev,
+ (RApp (dummy_loc,
(RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
| _ ->
match na with
@@ -1613,7 +1613,7 @@ let vars_of_ctx ctx =
ctx (id_of_string "vars_of_ctx_error", [])
in List.rev y
-let rec is_included x y =
+let rec is_included x y =
match x, y with
| PatVar _, _ -> true
| _, PatVar _ -> true
@@ -1626,12 +1626,12 @@ let rec is_included x y =
*)
let build_ineqs prevpatterns pats liftsign =
let _tomatchs = List.length pats in
- let diffs =
- List.fold_left
- (fun c eqnpats ->
+ let diffs =
+ List.fold_left
+ (fun c eqnpats ->
let acc = List.fold_left2
(* ppat is the pattern we are discriminating against, curpat is the current one. *)
- (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat)
+ (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat)
(curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) ->
match acc with
None -> None
@@ -1641,33 +1641,33 @@ let build_ineqs prevpatterns pats liftsign =
let lens = List.length ppat_sign in
(* Accumulated length of previous pattern's signatures *)
let len' = lens + len in
- let acc =
+ let acc =
((* Jump over previous prevpat signs *)
- lift_rel_context len ppat_sign @ sign,
+ lift_rel_context len ppat_sign @ sign,
len',
succ n, (* nth pattern *)
mkApp (Lazy.force eq_ind,
[| lift (len' + liftsign) curpat_ty;
liftn (len + liftsign) (succ lens) ppat_c ;
- lift len' curpat_c |]) ::
+ lift len' curpat_c |]) ::
List.map (lift lens (* Jump over this prevpat signature *)) c)
in Some acc
else None)
(Some ([], 0, 0, [])) eqnpats pats
- in match acc with
+ in match acc with
None -> c
| Some (sign, len, _, c') ->
- let conj = it_mkProd_or_LetIn (mk_not (mk_conj c'))
- (lift_rel_context liftsign sign)
+ let conj = it_mkProd_or_LetIn (mk_not (mk_conj c'))
+ (lift_rel_context liftsign sign)
in
conj :: c)
[] prevpatterns
in match diffs with [] -> None
| _ -> Some (mk_conj diffs)
-
+
let subst_rel_context k ctx subst =
let (_, ctx') =
- List.fold_right
+ List.fold_right
(fun (n, b, t) (k, acc) ->
(succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
ctx (k, [])
@@ -1683,29 +1683,29 @@ let lift_rel_contextn n k sign =
let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
let i = ref 0 in
- let (x, y, z) =
+ let (x, y, z) =
List.fold_left
(fun (branches, eqns, prevpatterns) eqn ->
- let _, newpatterns, pats =
+ let _, newpatterns, pats =
List.fold_left2
- (fun (idents, newpatterns, pats) pat arsign ->
+ (fun (idents, newpatterns, pats) pat arsign ->
let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in
(idents, pat' :: newpatterns, cpat :: pats))
([], [], []) eqn.patterns sign
in
let newpatterns = List.rev newpatterns and opats = List.rev pats in
- let rhs_rels, pats, signlen =
- List.fold_left
- (fun (renv, pats, n) (sign,c, (s, args), p) ->
+ let rhs_rels, pats, signlen =
+ List.fold_left
+ (fun (renv, pats, n) (sign,c, (s, args), p) ->
(* Recombine signatures and terms of all of the row's patterns *)
let sign' = lift_rel_context n sign in
let len = List.length sign' in
- (sign' @ renv,
+ (sign' @ renv,
(* lift to get outside of previous pattern's signatures. *)
(sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
len + n))
([], [], 0) opats in
- let pats, _ = List.fold_left
+ let pats, _ = List.fold_left
(* lift to get outside of past patterns to get terms in the combined environment. *)
(fun (pats, n) (sign, c, (s, args), p) ->
let len = List.length sign in
@@ -1716,7 +1716,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
let rhs_rels' = rels_of_patsign rhs_rels in
let _signenv = push_rel_context rhs_rels' env in
let arity =
- let args, nargs =
+ let args, nargs =
List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
(args @ c :: allargs, List.length args + succ n))
pats ([], 0)
@@ -1724,7 +1724,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
let args = List.rev args in
substl args (liftn signlen (succ nargs) arity)
in
- let rhs_rels', tycon =
+ let rhs_rels', tycon =
let neqs_rels, arity =
match ineqs with
| None -> [], arity
@@ -1740,7 +1740,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
- let branch =
+ let branch =
let bref = RVar (dummy_loc, branch_name) in
match vars_of_ctx rhs_rels with
[] -> bref
@@ -1767,30 +1767,30 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
* A type constraint but no annotation case: it is assumed non dependent.
*)
-
-let lift_ctx n ctx =
+
+let lift_ctx n ctx =
let ctx', _ =
List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0)
in ctx'
(* Turn matched terms into variables. *)
let abstract_tomatch env tomatchs tycon =
- let prev, ctx, names, tycon =
+ let prev, ctx, names, tycon =
List.fold_left
(fun (prev, ctx, names, tycon) (c, t) ->
let lenctx = List.length ctx in
match kind_of_term c with
Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
- | _ ->
+ | _ ->
let tycon = Option.map
(fun t -> subst_term_occ all_occurrences (lift 1 c) (lift 1 t)) tycon in
let name = next_ident_away_from (id_of_string "filtered_var") names in
- (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
- (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
+ (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
+ (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
name :: names, tycon)
([], [], [], tycon) tomatchs
in List.rev prev, ctx, tycon
-
+
let is_dependent_ind = function
IsInd (_, IndType (indf, args)) when List.length args > 0 -> true
| _ -> false
@@ -1800,13 +1800,13 @@ let build_dependent_signature env evars avoid tomatchs arsign =
let arsign = List.rev arsign in
let allnames = List.rev (List.map (List.map pi1) arsign) in
let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
- let eqs, neqs, refls, slift, arsign' =
- List.fold_left2
- (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign ->
+ let eqs, neqs, refls, slift, arsign' =
+ List.fold_left2
+ (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign ->
(* The accumulator:
- previous eqs,
- number of previous eqs,
- lift to get outside eqs and in the introduced variables ('as' and 'in'),
+ previous eqs,
+ number of previous eqs,
+ lift to get outside eqs and in the introduced variables ('as' and 'in'),
new arity signatures
*)
match ty with
@@ -1819,7 +1819,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
List.fold_left2
(fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
let argt = Retyping.get_type_of env evars arg in
- let eq, refl_arg =
+ let eq, refl_arg =
if Reductionops.is_conv env evars argt t then
(mk_eq (lift (nargeqs + slift) argt)
(mkRel (nargeqs + slift))
@@ -1832,58 +1832,58 @@ let build_dependent_signature env evars avoid tomatchs arsign =
(lift (nargeqs + nar) arg),
mk_JMeq_refl argt arg)
in
- let previd, id =
- let name =
- match kind_of_term arg with
+ let previd, id =
+ let name =
+ match kind_of_term arg with
Rel n -> pi1 (lookup_rel n env)
| _ -> name
in
- make_prime avoid name
+ make_prime avoid name
in
- (env, succ nargeqs,
- (Name (eq_id avoid previd), None, eq) :: argeqs,
+ (env, succ nargeqs,
+ (Name (eq_id avoid previd), None, eq) :: argeqs,
refl_arg :: refl_args,
pred slift,
(Name id, b, t) :: argsign'))
(env, 0, [], [], slift, []) args argsign
in
- let eq = mk_JMeq
+ let eq = mk_JMeq
(lift (nargeqs + slift) appt)
(mkRel (nargeqs + slift))
- (lift (nargeqs + nar) ty)
- (lift (nargeqs + nar) tm)
+ (lift (nargeqs + nar) ty)
+ (lift (nargeqs + nar) tm)
in
let refl_eq = mk_JMeq_refl ty tm in
let previd, id = make_prime avoid appn in
- (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
- succ nargeqs,
+ (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
+ succ nargeqs,
refl_eq :: refl_args,
- pred slift,
+ pred slift,
(((Name id, appb, appt) :: argsign') :: arsigns))
-
- | _ ->
+
+ | _ ->
(* Non dependent inductive or not inductive, just use a regular equality *)
let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
let previd, id = make_prime avoid name in
let arsign' = (Name id, b, typ) in
let tomatch_ty = type_of_tomatch ty in
- let eq =
+ let eq =
mk_eq (lift nar tomatch_ty)
(mkRel slift) (lift nar tm)
in
- ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
+ ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
(mk_eq_refl tomatch_ty tm) :: refl_args,
pred slift, (arsign' :: []) :: arsigns))
([], 0, [], nar, []) tomatchs arsign
- in
+ in
let arsign'' = List.rev arsign' in
assert(slift = 0); (* we must have folded over all elements of the arity signature *)
arsign'', allnames, nar, eqs, neqs, refls
(**************************************************************************)
(* Main entry of the matching compilation *)
-
-let liftn_rel_context n k sign =
+
+let liftn_rel_context n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
@@ -1891,16 +1891,16 @@ let liftn_rel_context n k sign =
in
liftrec (k + rel_context_length sign) sign
-let nf_evars_env evar_defs (env : env) : env =
+let nf_evars_env evar_defs (env : env) : env =
let nf t = nf_isevar evar_defs t in
- let env0 : env = reset_context env in
+ let env0 : env = reset_context env in
let f e (na, b, t) e' : env =
Environ.push_named (na, Option.map nf b, nf t) e'
in
let env' = Environ.fold_named_context f ~init:env0 env in
Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
~init:env' env
-
+
let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
(* We extract the signature of the arity *)
@@ -1910,12 +1910,12 @@ let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon
match rtntyp with
| Some rtntyp ->
let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
- let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ let predccl = (j_nf_isevar !isevars predcclj).uj_val in
Some (build_initial_predicate true allnames predccl)
- | None ->
+ | None ->
match valcon_of_tycon tycon with
- | Some ty ->
- let pred =
+ | Some ty ->
+ let pred =
prepare_predicate_from_arsign_tycon loc env !isevars tomatchs arsign ty
in Some (build_initial_predicate true allnames pred)
| None -> None
@@ -1926,7 +1926,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
(* We build the matrix of patterns and right-hand-side *)
let matx = matx_of_eqns env eqns in
-
+
(* We build the vector of terms to match consistently with the *)
(* constructors found in patterns *)
let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
@@ -1935,8 +1935,8 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
let tycon = valcon_of_tycon tycon in
let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in
let env = push_rel_context tomatchs_lets env in
- let len = List.length eqns in
- let sign, allnames, signlen, eqs, neqs, args =
+ let len = List.length eqns in
+ let sign, allnames, signlen, eqs, neqs, args =
(* The arity signature *)
let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in
(* Build the dependent arity signature, the equalities which makes
@@ -1945,21 +1945,21 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
build_dependent_signature env ( !isevars) avoid tomatchs arsign
in
- let tycon, arity =
+ let tycon, arity =
match tycon' with
| None -> let ev = mkExistential env isevars in ev, ev
- | Some t ->
+ | Some t ->
Option.get tycon, prepare_predicate_from_arsign_tycon loc env ( !isevars)
tomatchs sign t
in
- let neqs, arity =
+ let neqs, arity =
let ctx = context_of_arsign eqs in
let neqs = List.length ctx in
neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
in
- let lets, matx =
+ let lets, matx =
(* Type the rhs under the assumption of equations *)
- constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity
+ constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity
in
let matx = List.rev matx in
let _ = assert(len = List.length lets) in
@@ -1973,7 +1973,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
(* We push the initial terms to match and push their alias to rhs' envs *)
(* names of aliases will be recovered from patterns (hence Anonymous here) *)
let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-
+
let pb =
{ env = env;
isevars = isevars;
@@ -1984,12 +1984,12 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
caseloc = loc;
casestyle= style;
typing_function = typing_fun } in
-
+
let j = compile pb in
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
- let j =
+ let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
uj_type = nf_isevar !isevars tycon; }
in j
@@ -2012,11 +2012,11 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
caseloc = loc;
casestyle= style;
typing_function = typing_fun } in
-
+
let j = compile pb in
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
- inh_conv_coerce_to_tycon loc env isevars j tycon
-
+ inh_conv_coerce_to_tycon loc env isevars j tycon
+
end
-
+
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 2b76266718..6fe14da34d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -35,7 +35,7 @@ let interp_binder_evars evdref env na t =
let interp_binders_evars isevars env avoid l =
List.fold_left
- (fun (env, ids, params) ((loc, i), t) ->
+ (fun (env, ids, params) ((loc, i), t) ->
let n = Name i in
let t' = interp_binder_evars isevars env n t in
let d = (i,None,t') in
@@ -44,7 +44,7 @@ let interp_binders_evars isevars env avoid l =
let interp_typeclass_context_evars isevars env avoid l =
List.fold_left
- (fun (env, ids, params) (iid, bk, cl) ->
+ (fun (env, ids, params) (iid, bk, cl) ->
let t' = interp_binder_evars isevars env (snd iid) cl in
let i = match snd iid with
| Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
@@ -56,13 +56,13 @@ let interp_typeclass_context_evars isevars env avoid l =
let interp_constrs_evars isevars env avoid l =
List.fold_left
- (fun (env, ids, params) t ->
+ (fun (env, ids, params) t ->
let t' = interp_binder_evars isevars env Anonymous t in
let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
let d = (id,None,t') in
(push_named d env, id :: ids, d::params))
(env, avoid, []) l
-
+
let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
SPretyping.understand_tcc_evars evdref env kind
(intern_gen (kind=IsType) ~impls ( !evdref) env c)
@@ -99,11 +99,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
match bk with
| Implicit ->
Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *)
- ~allow_partial:false (fun avoid (clname, (id, _, t)) ->
- match clname with
- | Some (cl, b) ->
- let t =
- if b then
+ ~allow_partial:false (fun avoid (clname, (id, _, t)) ->
+ match clname with
+ | Some (cl, b) ->
+ let t =
+ if b then
let _k = class_info cl in
CHole (Util.dummy_loc, Some Evd.InternalHole)
else CHole (Util.dummy_loc, None)
@@ -113,21 +113,21 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
| Explicit -> cl
in
let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
- let k, ctx', imps, subst =
+ let k, ctx', imps, subst =
let c = Command.generalize_constr_expr tclass ctx in
let c', imps = interp_type_evars_impls ~evdref:isevars env c in
let ctx, c = decompose_prod_assum c' in
let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
cl, ctx, imps, (List.rev args)
in
- let id =
+ let id =
match snd instid with
- | Name id ->
+ | Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
id
- | Anonymous ->
+ | Anonymous ->
let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
Termops.next_global_ident_away false i (Termops.ids_of_context env)
in
@@ -136,29 +136,29 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
let sigma = !isevars in
let subst = List.map (Evarutil.nf_evar sigma) subst in
- let subst =
- let props =
+ let subst =
+ let props =
match props with
- | CRecord (loc, _, fs) ->
- if List.length fs > List.length k.cl_props then
+ | CRecord (loc, _, fs) ->
+ if List.length fs > List.length k.cl_props then
Classes.mismatched_props env' (List.map snd fs) k.cl_props;
fs
- | _ ->
- if List.length k.cl_props <> 1 then
+ | _ ->
+ if List.length k.cl_props <> 1 then
errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
in
- match k.cl_props with
- | [(na,b,ty)] ->
+ match k.cl_props with
+ | [(na,b,ty)] ->
let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in
let ty' = substl subst ty in
let c = interp_casted_constr_evars isevars env' term ty' in
c :: subst
| _ ->
- let props, rest =
+ let props, rest =
List.fold_left
- (fun (props, rest) (id,_,_) ->
- try
+ (fun (props, rest) (id,_,_) ->
+ try
let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
@@ -166,23 +166,23 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
([], props) k.cl_props
in
- if rest <> [] then
+ if rest <> [] then
unbound_method env' k.cl_impl (fst (List.hd rest))
else
fst (type_ctx_instance isevars env' k.cl_props props subst)
in
- let subst = List.fold_left2
+ let subst = List.fold_left2
(fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
[] subst (k.cl_props @ snd k.cl_context)
in
let inst_constr, ty_constr = instance_constructor k subst in
isevars := Evarutil.nf_evar_defs !isevars;
let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
- and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx')
+ and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx')
in
isevars := undefined_evars !isevars;
Evarutil.check_evars env Evd.empty !isevars termtype;
- let hook vis gr =
+ let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
let inst = Typeclasses.new_instance k pri global cst in
Impargs.declare_manual_implicits false gr ~enriching:false imps;
@@ -191,4 +191,4 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let evm = Subtac_utils.evars_of_term ( !isevars) Evd.empty term in
let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
-
+
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 917ed80594..eb9f3c8e38 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -32,7 +32,7 @@ val type_ctx_instance : Evd.evar_defs ref ->
Term.constr list *
('a * Term.constr option * Term.constr) list
-val new_instance :
+val new_instance :
?global:bool ->
local_binder list ->
typeclass_constraint ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index ce7b5431b1..4dd3dd32be 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -33,7 +33,7 @@ open Pp
let pair_of_array a = (a.(0), a.(1))
let make_name s = Name (id_of_string s)
-let rec disc_subset x =
+let rec disc_subset x =
match kind_of_term x with
| App (c, l) ->
(match kind_of_term c with
@@ -47,33 +47,33 @@ let rec disc_subset x =
else None
| _ -> None)
| _ -> None
-
+
and disc_exist env x =
match kind_of_term x with
| App (c, l) ->
(match kind_of_term c with
- Construct c ->
+ Construct c ->
if c = Term.destConstruct (Lazy.force sig_).intro
then Some (l.(0), l.(1), l.(2), l.(3))
else None
| _ -> None)
| _ -> None
-
+
module Coercion = struct
-
+
exception NoSubtacCoercion
-
+
let disc_proj_exist env x =
match kind_of_term x with
| App (c, l) ->
- (if Term.eq_constr c (Lazy.force sig_).proj1
- && Array.length l = 3
+ (if Term.eq_constr c (Lazy.force sig_).proj1
+ && Array.length l = 3
then disc_exist env l.(2)
else None)
| _ -> None
- let sort_rel s1 s2 =
+ let sort_rel s1 s2 =
match s1, s2 with
Prop Pos, Prop Pos -> Prop Pos
| Prop Pos, Prop Null -> Prop Null
@@ -92,27 +92,27 @@ module Coercion = struct
in
liftrec (List.length sign) sign
- let rec mu env isevars t =
+ let rec mu env isevars t =
let isevars = ref isevars in
- let rec aux v =
+ let rec aux v =
let v = hnf env isevars v in
match disc_subset v with
- Some (u, p) ->
+ Some (u, p) ->
let f, ct = aux u in
- (Some (fun x ->
- app_opt f (mkApp ((Lazy.force sig_).proj1,
+ (Some (fun x ->
+ app_opt f (mkApp ((Lazy.force sig_).proj1,
[| u; p; x |]))),
ct)
| None -> (None, v)
in aux t
- and coerce loc env isevars (x : Term.constr) (y : Term.constr)
- : (Term.constr -> Term.constr) option
+ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
+ : (Term.constr -> Term.constr) option
=
let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
let rec coerce_unify env x y =
let x = hnf env isevars x and y = hnf env isevars y in
- try
+ try
isevars := the_conv_x_leq env x y !isevars;
None
with Reduction.NotConvertible -> coerce' env x y
@@ -125,7 +125,7 @@ module Coercion = struct
in
let rec coerce_application typ typ' c c' l l' =
let len = Array.length l in
- let rec aux tele typ typ' i co =
+ let rec aux tele typ typ' i co =
if i < len then
let hdx = l.(i) and hdy = l'.(i) in
try isevars := the_conv_x_leq env hdx hdy !isevars;
@@ -135,15 +135,15 @@ module Coercion = struct
with Reduction.NotConvertible ->
let (n, eqT), restT = dest_prod typ in
let (n', eqT'), restT' = dest_prod typ' in
- let _ =
+ let _ =
try isevars := the_conv_x_leq env eqT eqT' !isevars
with Reduction.NotConvertible -> raise NoSubtacCoercion
in
(* Disallow equalities on arities *)
if Reduction.is_arity env eqT then raise NoSubtacCoercion;
- let restargs = lift_args 1
+ let restargs = lift_args 1
(List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
- in
+ in
let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in
let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
@@ -152,14 +152,14 @@ module Coercion = struct
[| eqT; hdx; pred; x; hdy; evar|]) in
aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some co
- in
+ in
if isEvar c || isEvar c' then
(* Second-order unification needed. *)
raise NoSubtacCoercion;
aux [] typ typ' 0 (fun x -> x)
in
match (kind_of_term x, kind_of_term y) with
- | Sort s, Sort s' ->
+ | Sort s, Sort s' ->
(match s, s' with
Prop x, Prop y when x = y -> None
| Prop _, Type _ -> None
@@ -178,11 +178,11 @@ module Coercion = struct
None, None -> failwith "subtac.coerce': Should have detected equivalence earlier"
| _, _ ->
Some
- (fun f ->
+ (fun f ->
mkLambda (name', a',
app_opt c2
(mkApp (Term.lift 1 f, [| coec1 |])))))
-
+
| App (c, l), App (c', l') ->
(match kind_of_term c, kind_of_term c' with
Ind i, Ind i' -> (* Inductive types *)
@@ -192,16 +192,16 @@ module Coercion = struct
(* Sigma types *)
if len = Array.length l' && len = 2 && i = i'
&& (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
- then
- if i = Term.destInd existS.typ
+ then
+ if i = Term.destInd existS.typ
then
- begin
- let (a, pb), (a', pb') =
- pair_of_array l, pair_of_array l'
+ begin
+ let (a, pb), (a', pb') =
+ pair_of_array l, pair_of_array l'
in
let c1 = coerce_unify env a a' in
- let rec remove_head a c =
- match kind_of_term c with
+ let rec remove_head a c =
+ match kind_of_term c with
| Lambda (n, t, t') -> c, t'
(*| Prod (n, t, t') -> t'*)
| Evar (k, args) ->
@@ -217,35 +217,35 @@ module Coercion = struct
let env' = push_rel (make_name "x", None, a) env in
let c2 = coerce_unify env' b b' in
match c1, c2 with
- None, None ->
+ None, None ->
None
| _, _ ->
- Some
+ Some
(fun x ->
- let x, y =
+ let x, y =
app_opt c1 (mkApp (existS.proj1,
[| a; pb; x |])),
- app_opt c2 (mkApp (existS.proj2,
+ app_opt c2 (mkApp (existS.proj2,
[| a; pb; x |]))
in
mkApp (existS.intro, [| a'; pb'; x ; y |]))
end
- else
- begin
- let (a, b), (a', b') =
- pair_of_array l, pair_of_array l'
+ else
+ begin
+ let (a, b), (a', b') =
+ pair_of_array l, pair_of_array l'
in
let c1 = coerce_unify env a a' in
let c2 = coerce_unify env b b' in
match c1, c2 with
None, None -> None
| _, _ ->
- Some
+ Some
(fun x ->
- let x, y =
+ let x, y =
app_opt c1 (mkApp (prod.proj1,
[| a; b; x |])),
- app_opt c2 (mkApp (prod.proj2,
+ app_opt c2 (mkApp (prod.proj2,
[| a; b; x |]))
in
mkApp (prod.intro, [| a'; b'; x ; y |]))
@@ -253,7 +253,7 @@ module Coercion = struct
else
if i = i' && len = Array.length l' then
let evm = !isevars in
- (try subco ()
+ (try subco ()
with NoSubtacCoercion ->
let typ = Typing.type_of env evm c in
let typ' = Typing.type_of env evm c' in
@@ -276,25 +276,25 @@ module Coercion = struct
and subset_coerce env isevars x y =
match disc_subset x with
- Some (u, p) ->
+ Some (u, p) ->
let c = coerce_unify env u y in
- let f x =
- app_opt c (mkApp ((Lazy.force sig_).proj1,
+ let f x =
+ app_opt c (mkApp ((Lazy.force sig_).proj1,
[| u; p; x |]))
in Some f
| None ->
match disc_subset y with
Some (u, p) ->
let c = coerce_unify env x u in
- Some
+ Some
(fun x ->
let cx = app_opt c x in
let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
in
- (mkApp
- ((Lazy.force sig_).intro,
+ (mkApp
+ ((Lazy.force sig_).intro,
[| u; p; cx; evar |])))
- | None ->
+ | None ->
raise NoSubtacCoercion
(*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
None*)
@@ -304,7 +304,7 @@ module Coercion = struct
let evars = ref isevars in
let coercion = coerce loc env evars t c1 in
!evars, Option.map (app_opt coercion) v
-
+
(* Taken from pretyping/coercion.ml *)
(* Typing operations dealing with coercions *)
@@ -317,11 +317,11 @@ module Coercion = struct
| h::restl ->
(* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
- | Prod (_,c1,c2) ->
+ | Prod (_,c1,c2) ->
(* Typage garanti par l'appel à app_coercion*)
apply_rec (h::acc) (subst1 h c2) restl
| _ -> anomaly "apply_coercion_args"
- in
+ in
apply_rec [] funj.uj_type argl
(* appliquer le chemin de coercions de patterns p *)
@@ -342,21 +342,21 @@ module Coercion = struct
(* appliquer le chemin de coercions p à hj *)
let apply_coercion env sigma p hj typ_cl =
- try
+ try
fst (List.fold_left
- (fun (ja,typ_cl) i ->
+ (fun (ja,typ_cl) i ->
let fv,isid = coercion_value i in
let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
let jres = apply_coercion_args env argl fv in
- (if isid then
+ (if isid then
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
- else
+ else
jres),
jres.uj_type)
(hj,typ_cl) p)
with _ -> anomaly "apply_coercion"
- let inh_app_fun env isevars j =
+ let inh_app_fun env isevars j =
let t = whd_betadeltaiota env ( isevars) j.uj_type in
match kind_of_term t with
| Prod (_,_,_) -> (isevars,j)
@@ -369,7 +369,7 @@ module Coercion = struct
lookup_path_to_fun_from env ( isevars) j.uj_type in
(isevars,apply_coercion env ( isevars) p j t)
with Not_found ->
- try
+ try
let coercef, t = mu env isevars t in
(isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
with NoSubtacCoercion | NoCoercion ->
@@ -378,7 +378,7 @@ module Coercion = struct
let inh_tosort_force loc env isevars j =
try
let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
- let j1 = apply_coercion env ( isevars) p j t in
+ let j1 = apply_coercion env ( isevars) p j t in
(isevars,type_judgment env (j_nf_evar ( isevars) j1))
with Not_found ->
error_not_a_type_loc loc env ( isevars) j
@@ -396,29 +396,29 @@ module Coercion = struct
let inh_coerce_to_base loc env isevars j =
let typ = whd_betadeltaiota env ( isevars) j.uj_type in
let ct, typ' = mu env isevars typ in
- isevars, { uj_val = app_opt ct j.uj_val;
+ isevars, { uj_val = app_opt ct j.uj_val;
uj_type = typ' }
let inh_coerce_to_prod loc env isevars t =
let typ = whd_betadeltaiota env ( isevars) (snd t) in
let _, typ' = mu env isevars typ in
isevars, (fst t, typ')
-
+
let inh_coerce_to_fail env evd rigidonly v t c1 =
if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
then
raise NoCoercion
else
let v', t' =
- try
+ try
let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
match v with
- Some v ->
+ Some v ->
let j = apply_coercion env ( evd) p
{uj_val = v; uj_type = t} t2 in
Some j.uj_val, j.uj_type
| None -> None, t
- with Not_found -> raise NoCoercion
+ with Not_found -> raise NoCoercion
in
try (the_conv_x_leq env t' c1 evd, v')
with Reduction.NotConvertible -> raise NoCoercion
@@ -433,12 +433,12 @@ module Coercion = struct
kind_of_term (whd_betadeltaiota env ( evd) t),
kind_of_term (whd_betadeltaiota env ( evd) c1)
with
- | Prod (name,t1,t2), Prod (_,u1,u2) ->
+ | Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
(* We eta-expand (hence possibly modifying the original term!) *)
(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
(* has type forall (x:u1), u2 (with v' recursively obtained) *)
- let name = match name with
+ let name = match name with
| Anonymous -> Name (id_of_string "x")
| _ -> name in
let env1 = push_rel (name,None,u1) env in
@@ -456,8 +456,8 @@ module Coercion = struct
let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
match n with
None ->
- let (evd', val') =
- try
+ let (evd', val') =
+ try
inh_conv_coerce_to_fail loc env evd rigidonly
(Some (nf_isevar evd cj.uj_val))
(nf_isevar evd cj.uj_type) (nf_isevar evd t)
@@ -482,7 +482,7 @@ module Coercion = struct
None -> 0, 0
| Some (init, cur) -> init, cur
in
- try
+ try
let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in
(* The final range free variables must have been replaced by evars, we accept only that evars
in rng are applied to free vars. *)
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 1095b143cc..d1e890867c 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -55,11 +55,11 @@ let evar_nf isevars c =
let get_undefined_evars evd =
Evd.fold (fun ev evi evd' ->
- if evi.evar_body = Evar_empty then
+ if evi.evar_body = Evar_empty then
Evd.add evd' ev (nf_evar_info evd evi)
else evd') evd Evd.empty
-let interp_gen kind isevars env
+let interp_gen kind isevars env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
@@ -67,16 +67,16 @@ let interp_gen kind isevars env
evar_nf isevars c'
let interp_constr isevars env c =
- interp_gen (OfType None) isevars env c
+ interp_gen (OfType None) isevars env c
let interp_type_evars isevars env ?(impls=([],[])) c =
interp_gen IsType isevars env ~impls c
let interp_casted_constr isevars env ?(impls=([],[])) c typ =
- interp_gen (OfType (Some typ)) isevars env ~impls c
+ interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
- interp_gen (OfType (Some typ)) isevars env ~impls c
+ interp_gen (OfType (Some typ)) isevars env ~impls c
let interp_open_constr isevars env c =
msgnl (str "Pretyping " ++ my_print_constr_expr c);
@@ -85,17 +85,17 @@ let interp_open_constr isevars env c =
evar_nf isevars c'
let interp_constr_judgment isevars env c =
- let j =
+ let j =
SPretyping.understand_judgment_tcc isevars env
- (Constrintern.intern_constr ( !isevars) env c)
+ (Constrintern.intern_constr ( !isevars) env c)
in
{ uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
let locate_if_isevar loc na = function
- | RHole _ ->
+ | RHole _ ->
(try match na with
| Name id -> Reserve.find_reserved_type id
- | Anonymous -> raise Not_found
+ | Anonymous -> raise Not_found
with Not_found -> RHole (loc, Evd.BinderType na))
| x -> x
@@ -103,7 +103,7 @@ let interp_binder sigma env na t =
let t = Constrintern.intern_gen true ( !sigma) env t in
SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
-let interp_context_evars evdref env params =
+let interp_context_evars evdref env params =
let bl = Constrintern.intern_context false ( !evdref) env params in
let (env, par, _, impls) =
List.fold_left
@@ -113,7 +113,7 @@ let interp_context_evars evdref env params =
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
let t = SPretyping.understand_tcc_evars evdref env IsType t' in
let d = (na,None,t) in
- let impls =
+ let impls =
if k = Implicit then
let na = match na with Name n -> Some n | Anonymous -> None in
(ExplByPos (n, na), (true, true, true)) :: impls
@@ -134,39 +134,39 @@ let list_chop_hd i l = match list_chop i l with
| (x :: [], l2) -> ([], x, [])
| _ -> assert(false)
-let collect_non_rec env =
- let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
+let collect_non_rec env =
+ let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
try
- let i =
+ let i =
list_try_find_i
(fun i f ->
if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
then i else failwith "try_find_i")
- 0 lnamerec
+ 0 lnamerec
in
let (lf1,f,lf2) = list_chop_hd i lnamerec in
let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
let (lar1,ar,lar2) = list_chop_hd i larrec in
- let newlnv =
- try
- match list_chop i nrec with
+ let newlnv =
+ try
+ match list_chop i nrec with
| (lnv1,_::lnv2) -> (lnv1@lnv2)
| _ -> [] (* nrec=[] for cofixpoints *)
with Failure "list_chop" -> []
- in
- searchrec ((f,def,ar)::lnonrec)
+ in
+ searchrec ((f,def,ar)::lnonrec)
(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
- with Failure "try_find_i" ->
+ with Failure "try_find_i" ->
(List.rev lnonrec,
(Array.of_list lnamerec, Array.of_list ldefrec,
Array.of_list larrec, Array.of_list nrec))
- in
- searchrec []
+ in
+ searchrec []
-let list_of_local_binders l =
+let list_of_local_binders l =
let rec aux acc = function
Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
- | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
+ | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
| [] -> List.rev acc
in aux [] l
@@ -201,7 +201,7 @@ let telescope = function
| (n, None, t) :: tl ->
let ty, tys, (k, constr) =
List.fold_left
- (fun (ty, tys, (k, constr)) (n, b, t) ->
+ (fun (ty, tys, (k, constr)) (n, b, t) ->
let pred = mkLambda (n, t, ty) in
let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
@@ -215,14 +215,14 @@ let telescope = function
(lift 1 proj2, (n, Some proj1, t) :: subst))
(List.rev tys) tl (mkRel 1, [])
in ty, ((n, Some last, t) :: subst), constr
-
+
| _ -> raise (Invalid_argument "telescope")
let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let sigma = Evd.empty in
let isevars = ref (Evd.create_evar_defs sigma) in
- let env = Global.env() in
+ let env = Global.env() in
let _pr c = my_print_constr env c in
let _prr = Printer.pr_rel_context env in
let _prn = Printer.pr_named_context env in
@@ -235,8 +235,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let argtyp, letbinders, make = telescope binders_rel in
let argname = id_of_string "recarg" in
let arg = (Name argname, None, argtyp) in
- let wrapper x =
- if List.length binders_rel > 1 then
+ let wrapper x =
+ if List.length binders_rel > 1 then
it_mkLambda_or_LetIn (mkApp (x, [|make|])) binders_rel
else x
in
@@ -244,12 +244,12 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let binders_env = push_rel_context binders_rel env in
let rel = interp_constr isevars env r in
let relty = type_of env !isevars rel in
- let relargty =
+ let relargty =
let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
match ctx, kind_of_term ar with
- | [(_, None, t); (_, None, u)], Sort (Prop Null)
+ | [(_, None, t); (_, None, u)], Sort (Prop Null)
when Reductionops.is_conv env !isevars t u -> t
- | _, _ ->
+ | _, _ ->
user_err_loc (constr_loc r,
"Subtac_command.build_wellfounded",
my_print_constr env rel ++ str " is not an homogeneous binary relation.")
@@ -261,7 +261,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
it_mkLambda_or_LetIn measure binders
in
let comb = constr_of_global (Lazy.force measure_on_R_ref) in
- let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
+ let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
mkApp (rel, [| subst1 x measure_body;
subst1 y measure_body |])
@@ -280,13 +280,13 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
in
- let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
+ let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
let intern_arity = substl [projection] top_arity_let in
(* substitute the projection of wfarg for something,
now intern_arity is in wfarg :: arg *)
let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
- let curry_fun =
+ let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
@@ -298,22 +298,22 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
in
let fun_bl = intern_fun_binder :: [arg] in
let lift_lets = Termops.lift_rel_context 1 letbinders in
- let intern_body =
+ let intern_body =
let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
let impls = Command.compute_interning_datas env Constrintern.Recursive [] [recname] [full_arity] [impls] in
- let newimpls =
+ let newimpls =
match snd impls with
[(p, (r, l, impls, scopes))] ->
[(p, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))]
| x -> x
- in interp_casted_constr isevars ~impls:(fst impls,newimpls)
+ in interp_casted_constr isevars ~impls:(fst impls,newimpls)
(push_rel_context ctx env) body (lift 1 top_arity)
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let fix_def =
mkApp (constr_of_global (Lazy.force fix_sub_ref),
- [| argtyp ; wf_rel ;
+ [| argtyp ; wf_rel ;
make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
prop ; intern_body_lam |])
in
@@ -328,10 +328,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
-let nf_evar_context isevars ctx =
- List.map (fun (n, b, t) ->
+let nf_evar_context isevars ctx =
+ List.map (fun (n, b, t) ->
(n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
-
+
let interp_fix_context evdref env fix =
interp_context_evars evdref env fix.Command.fix_binders
@@ -350,7 +350,7 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
let names = List.map (fun id -> Name id) fixnames in
(Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
-let rel_index n ctx =
+let rel_index n ctx =
list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
let rec unfold f b =
@@ -359,16 +359,16 @@ let rec unfold f b =
| None -> []
let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
- match n with
+ match n with
| Some (loc, n) -> [rel_index n fixctx]
- | None ->
+ | None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
- but doing it properly involves delta-reduction, and it finally
- doesn't seem to worth the effort (except for huge mutual
+ but doing it properly involves delta-reduction, and it finally
+ doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
let len = List.length fixctx in
- unfold (function x when x = len -> None
+ unfold (function x when x = len -> None
| n -> Some (n, succ n)) 0
let push_named_context = List.fold_right push_named
@@ -402,11 +402,11 @@ let interp_recursive fixkind l boxed =
let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
- let rec_sign =
+ let rec_sign =
List.fold_left2 (fun env' id t ->
let sort = Retyping.get_type_of env !evdref t in
- let fixprot =
- try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|])
+ let fixprot =
+ try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|])
with e -> t
in
(id,None,fixprot) :: env')
@@ -419,8 +419,8 @@ let interp_recursive fixkind l boxed =
let notations = List.fold_right Option.List.cons ntnl [] in
(* Interp bodies with rollback because temp use of notations/implicit *)
- let fixdefs =
- States.with_state_protection (fun () ->
+ let fixdefs =
+ States.with_state_protection (fun () ->
List.iter (Command.declare_interning_data impls) notations;
list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
() in
@@ -434,7 +434,7 @@ let interp_recursive fixkind l boxed =
let fixdefs = List.map (nf_evar evd) fixdefs in
let fixtypes = List.map (nf_evar evd) fixtypes in
let rec_sign = nf_named_context_evar evd rec_sign in
-
+
let recdefs = List.length rec_sign in
List.iter (check_evars env_rec Evd.empty evd) fixdefs;
List.iter (check_evars env Evd.empty evd) fixtypes;
@@ -446,9 +446,9 @@ let interp_recursive fixkind l boxed =
let isevars = Evd.undefined_evars evd in
let evm = isevars in
(* Solve remaining evars *)
- let rec collect_evars id def typ imps =
+ let rec collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
- let def =
+ let def =
Termops.it_mkNamedLambda_or_LetIn def rec_sign
and typ =
Termops.it_mkNamedProd_or_LetIn typ rec_sign
@@ -457,14 +457,14 @@ let interp_recursive fixkind l boxed =
let evm' = Subtac_utils.evars_of_term evm evm' typ in
let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
(id, def, typ, imps, evars)
- in
+ in
let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
(match fixkind with
| Command.IsFixpoint wfl ->
let possible_indexes =
list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
- let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
- Array.of_list fixtypes,
+ let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
+ Array.of_list fixtypes,
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
in
let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
@@ -480,8 +480,8 @@ let build_recursive l b =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
- ignore(build_wellfounded (id, n, bl, typ, def) r
- (match n with Some n -> mkIdentC (snd n) | None ->
+ ignore(build_wellfounded (id, n, bl, typ, def) r
+ (match n with Some n -> mkIdentC (snd n) | None ->
errorlabstrm "Subtac_command.build_recursive"
(str "Recursive argument required for well-founded fixpoints"))
ntn false)
@@ -491,15 +491,15 @@ let build_recursive l b =
m ntn false)
| _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
- let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
- ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l
+ let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
+ ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l
in interp_recursive (Command.IsFixpoint g) fixl b
- | _, _ ->
+ | _, _ ->
errorlabstrm "Subtac_command.build_recursive"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
let build_corecursive l b =
- let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
+ let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
l in
interp_recursive Command.IsCoFixpoint fixl b
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 6f73bc9424..6c0c4340f9 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -47,7 +47,7 @@ val telescope :
Term.types * (Names.name * Term.types option * Term.types) list *
Term.constr
-val build_wellfounded :
+val build_wellfounded :
Names.identifier * 'a * Topconstr.local_binder list *
Topconstr.constr_expr * Topconstr.constr_expr ->
Topconstr.constr_expr ->
diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml
index 3bbfe22bc0..067da150ec 100644
--- a/plugins/subtac/subtac_errors.ml
+++ b/plugins/subtac/subtac_errors.ml
@@ -4,12 +4,12 @@ open Printer
type term_pp = Pp.std_ppcmds
-type subtyping_error =
+type subtyping_error =
| UncoercibleInferType of loc * term_pp * term_pp
| UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp
| UncoercibleRewrite of term_pp * term_pp
-type typing_error =
+type typing_error =
| NonFunctionalApp of loc * term_pp * term_pp * term_pp
| NonConvertible of loc * term_pp * term_pp
| NonSigma of loc * term_pp
@@ -17,7 +17,7 @@ type typing_error =
exception Subtyping_error of subtyping_error
exception Typing_error of typing_error
-
+
exception Debug_msg of string
let typing_error e = raise (Typing_error e)
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index fb74867f1b..94bd059c2d 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -29,7 +29,7 @@ let explain_no_obligations = function
type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
* Tacexpr.raw_tactic_expr option) array
-
+
type obligation =
{ obl_name : identifier;
obl_type : types;
@@ -74,18 +74,18 @@ let get_proofs_transparency () = !proofs_transparency
open Goptions
let _ =
- declare_bool_option
+ declare_bool_option
{ optsync = true;
optname = "transparency of Program obligations";
optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
- optwrite = set_proofs_transparency; }
+ optwrite = set_proofs_transparency; }
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
let get_obligation_body expand obl =
let c = Option.get obl.obl_body in
- if expand && obl.obl_status = Expand then
+ if expand && obl.obl_status = Expand then
match kind_of_term c with
| Const c -> constant_value (Global.env ()) c
| _ -> c
@@ -96,14 +96,14 @@ let subst_deps expand obls deps t =
Intset.fold
(fun x acc ->
let xobl = obls.(x) in
- let oblb =
+ let oblb =
try get_obligation_body expand xobl
with _ -> assert(false)
in (xobl.obl_name, oblb) :: acc)
deps []
in(* Termops.it_mkNamedProd_or_LetIn t subst *)
Term.replace_vars subst t
-
+
let subst_deps_obl obls obl =
let t' = subst_deps false obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
@@ -114,19 +114,19 @@ let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-let map_cardinal m =
- let i = ref 0 in
+let map_cardinal m =
+ let i = ref 0 in
ProgMap.iter (fun _ _ -> incr i) m;
!i
exception Found of program_info
-let map_first m =
+let map_first m =
try
ProgMap.iter (fun _ v -> raise (Found v)) m;
assert(false)
with Found x -> x
-
+
let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
let freeze () = !from_prg, !default_tactic_expr
@@ -140,7 +140,7 @@ let init () =
let _ = init ()
-let _ =
+let _ =
Summary.declare_summary "program-tcc-table"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
@@ -155,10 +155,10 @@ let cache (_, (infos, tac)) =
let load (_, (_, tac)) =
set_default_tactic tac
-let subst (_, s, (infos, tac)) =
+let subst (_, s, (infos, tac)) =
(infos, Tacinterp.subst_tactic s tac)
-let (input,output) =
+let (input,output) =
declare_object
{ (default_object "Program state") with
cache_function = cache;
@@ -173,40 +173,40 @@ let (input,output) =
subst_function = subst;
export_function = (fun x -> Some x) }
-let update_state () =
+let update_state () =
(* msgnl (str "Updating obligations info"); *)
Lib.add_anonymous_leaf (input (!from_prg, !default_tactic_expr))
-let set_default_tactic t =
+let set_default_tactic t =
set_default_tactic t; update_state ()
-
+
open Evd
-let progmap_remove prg =
+let progmap_remove prg =
from_prg := ProgMap.remove prg.prg_name !from_prg
-
+
let rec intset_to = function
-1 -> Intset.empty
| n -> Intset.add n (intset_to (pred n))
-
-let subst_body expand prg =
+
+let subst_body expand prg =
let obls, _ = prg.prg_obligations in
let ints = intset_to (pred (Array.length obls)) in
subst_deps expand obls ints prg.prg_body,
subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
-
+
let declare_definition prg =
let body, typ = subst_body false prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
- my_print_constr (Global.env()) body ++ str " : " ++
+ my_print_constr (Global.env()) body ++ str " : " ++
my_print_constr (Global.env()) prg.prg_type);
with _ -> ());
let (local, boxed, kind) = prg.prg_kind in
- let ce =
+ let ce =
{ const_entry_body = body;
const_entry_type = Some typ;
const_entry_opaque = false;
- const_entry_boxed = boxed}
+ const_entry_boxed = boxed}
in
(Command.get_declare_definition_hook ()) ce;
match local with
@@ -215,15 +215,15 @@ let declare_definition prg =
SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in
print_message (Subtac_utils.definition_message prg.prg_name);
- if Pfedit.refining () then
- Flags.if_verbose msg_warning
- (str"Local definition " ++ Nameops.pr_id prg.prg_name ++
+ if Pfedit.refining () then
+ Flags.if_verbose msg_warning
+ (str"Local definition " ++ Nameops.pr_id prg.prg_name ++
str" is not visible from current goals");
progmap_remove prg; update_state ();
VarRef prg.prg_name
| (Global|Local) ->
let c =
- Declare.declare_constant
+ Declare.declare_constant
prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
in
let gr = ConstRef c in
@@ -243,15 +243,15 @@ let rec lam_index n t acc =
if na = Name n then acc
else lam_index n b (succ acc)
| _ -> raise Not_found
-
+
let compute_possible_guardness_evidences (n,_) fixbody fixtype =
- match n with
+ match n with
| Some (loc, n) -> [lam_index n fixbody 0]
- | None ->
+ | None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
- but doing it properly involves delta-reduction, and it finally
- doesn't seem to worth the effort (except for huge mutual
+ but doing it properly involves delta-reduction, and it finally
+ doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
let m = Term.nb_prod fixtype in
let ctx = fst (decompose_prod_n_assum m fixtype) in
@@ -263,9 +263,9 @@ let reduce_fix =
let declare_mutual_definition l =
let len = List.length l in
let first = List.hd l in
- let fixdefs, fixtypes, fiximps =
+ let fixdefs, fixtypes, fiximps =
list_split3
- (List.map (fun x ->
+ (List.map (fun x ->
let subs, typ = (subst_body false x) in
(strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
in
@@ -285,7 +285,7 @@ let declare_mutual_definition l =
Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
| IsCoFixpoint ->
None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
- in
+ in
(* Declare the recursive definitions *)
let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
@@ -293,36 +293,36 @@ let declare_mutual_definition l =
Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
- first.prg_hook local gr;
+ first.prg_hook local gr;
List.iter progmap_remove l;
update_state (); kn
-
+
let declare_obligation obl body =
match obl.obl_status with
| Expand -> { obl with obl_body = Some body }
| Define opaque ->
- let ce =
+ let ce =
{ const_entry_body = body;
const_entry_type = Some obl.obl_type;
- const_entry_opaque =
- (if get_proofs_transparency () then false
+ const_entry_opaque =
+ (if get_proofs_transparency () then false
else opaque) ;
- const_entry_boxed = false}
+ const_entry_boxed = false}
in
- let constant = Declare.declare_constant obl.obl_name
+ let constant = Declare.declare_constant obl.obl_name
(DefinitionEntry ce,IsProof Property)
in
print_message (Subtac_utils.definition_message obl.obl_name);
{ obl with obl_body = Some (mkConst constant) }
-
+
let red = Reductionops.nf_betaiota Evd.empty
let init_prog_info n b t deps fixkind notations obls impls kind hook =
- let obls' =
+ let obls' =
Array.mapi
(fun i (n, t, l, o, d, tac) ->
debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
- { obl_name = n ; obl_body = None;
+ { obl_name = n ; obl_body = None;
obl_location = l; obl_type = red t; obl_status = o;
obl_deps = d; obl_tac = tac })
obls
@@ -330,30 +330,30 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook =
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
-
+
let get_prog name =
let prg_infos = !from_prg in
match name with
- Some n ->
+ Some n ->
(try ProgMap.find n prg_infos
with Not_found -> raise (NoObligations (Some n)))
- | None ->
+ | None ->
(let n = map_cardinal prg_infos in
- match n with
+ match n with
0 -> raise (NoObligations None)
| 1 -> map_first prg_infos
| _ -> error "More than one program with unsolved obligations")
-let get_prog_err n =
+let get_prog_err n =
try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
let obligations_solved prg = (snd prg.prg_obligations) = 0
-
-type progress =
- | Remain of int
+
+type progress =
+ | Remain of int
| Dependent
| Defined of global_reference
-
+
let obligations_message rem =
if rem > 0 then
if rem = 1 then
@@ -363,7 +363,7 @@ let obligations_message rem =
else
Flags.if_verbose msgnl (str "No more obligations remaining")
-let update_obls prg obls rem =
+let update_obls prg obls rem =
let prg' = { prg with prg_obligations = (obls, rem) } in
from_prg := map_replace prg.prg_name prg' !from_prg;
obligations_message rem;
@@ -379,12 +379,12 @@ let update_obls prg obls rem =
let kn = declare_mutual_definition progs in
Defined (ConstRef kn)
else Dependent)
-
+
let is_defined obls x = obls.(x).obl_body <> None
-let deps_remaining obls deps =
+let deps_remaining obls deps =
Intset.fold
- (fun x acc ->
+ (fun x acc ->
if is_defined obls x then acc
else x :: acc)
deps []
@@ -392,18 +392,18 @@ let deps_remaining obls deps =
let has_dependencies obls n =
let res = ref false in
Array.iteri
- (fun i obl ->
+ (fun i obl ->
if i <> n && Intset.mem n obl.obl_deps then
res := true)
obls;
!res
-
+
let kind_of_opacity o =
match o with
| Define false | Expand -> Subtac_utils.goal_kind
| _ -> Subtac_utils.goal_proof_kind
-let not_transp_msg =
+let not_transp_msg =
str "Obligation should be transparent but was declared opaque." ++ spc () ++
str"Use 'Defined' instead."
@@ -415,15 +415,15 @@ let rec solve_obligation prg num =
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
if obl.obl_body <> None then
- pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
+ pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
else
match deps_remaining obls obl.obl_deps with
| [] ->
let obl = subst_deps_obl obls obl in
Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
- (fun strength gr ->
+ (fun strength gr ->
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
- let obl =
+ let obl =
let transparent = evaluable_constant cst (Global.env ()) in
let body =
match obl.obl_status with
@@ -437,8 +437,8 @@ let rec solve_obligation prg num =
in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
- let res = try update_obls prg obls (pred rem)
- with e -> pperror (Cerrors.explain_exn e)
+ let res = try update_obls prg obls (pred rem)
+ with e -> pperror (Cerrors.explain_exn e)
in
match res with
| Remain n when n > 0 ->
@@ -451,7 +451,7 @@ let rec solve_obligation prg num =
Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
-
+
and subtac_obligation (user_num, name, typ) =
let num = pred user_num in
let prg = get_prog_err name in
@@ -462,20 +462,20 @@ and subtac_obligation (user_num, name, typ) =
None -> solve_obligation prg num
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
-
-
+
+
and solve_obligation_by_tac prg obls i tac =
let obl = obls.(i) in
- match obl.obl_body with
+ match obl.obl_body with
| Some _ -> false
- | None ->
+ | None ->
try
if deps_remaining obls obl.obl_deps = [] then
let obl = subst_deps_obl obls obl in
- let tac =
+ let tac =
match tac with
| Some t -> t
- | None ->
+ | None ->
match obl.obl_tac with
| Some t -> Tacinterp.interp t
| None -> !default_tactic
@@ -491,39 +491,39 @@ and solve_obligation_by_tac prg obls i tac =
user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
| e -> false
-and solve_prg_obligations prg tac =
+and solve_prg_obligations prg tac =
let obls, rem = prg.prg_obligations in
let rem = ref rem in
let obls' = Array.copy obls in
- let _ =
- Array.iteri (fun i x ->
+ let _ =
+ Array.iteri (fun i x ->
if solve_obligation_by_tac prg obls' i tac then
decr rem)
obls'
in
update_obls prg obls' !rem
-and solve_obligations n tac =
+and solve_obligations n tac =
let prg = get_prog_err n in
solve_prg_obligations prg tac
-and solve_all_obligations tac =
+and solve_all_obligations tac =
ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
-
-and try_solve_obligation n prg tac =
- let prg = get_prog prg in
+
+and try_solve_obligation n prg tac =
+ let prg = get_prog prg in
let obls, rem = prg.prg_obligations in
let obls' = Array.copy obls in
if solve_obligation_by_tac prg obls' n tac then
ignore(update_obls prg obls' (pred rem));
-and try_solve_obligations n tac =
+and try_solve_obligations n tac =
try ignore (solve_obligations n tac) with NoObligations _ -> ()
and auto_solve_obligations n tac : progress =
Flags.if_verbose msgnl (str "Solving obligations automatically...");
try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
-
+
open Pp
let show_obligations ?(msg=true) n =
let prg = get_prog_err n in
@@ -531,17 +531,17 @@ let show_obligations ?(msg=true) n =
let obls, rem = prg.prg_obligations in
let showed = ref 5 in
if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
- Array.iteri (fun i x ->
- match x.obl_body with
- | None ->
+ Array.iteri (fun i x ->
+ match x.obl_body with
+ | None ->
if !showed > 0 then (
decr showed;
msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
- str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
+ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
| Some _ -> ())
obls
-
+
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
@@ -554,19 +554,19 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
let prg = init_prog_info n b t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
- Flags.if_verbose ppnl (str ".");
- let cst = declare_definition prg in
+ Flags.if_verbose ppnl (str ".");
+ let cst = declare_definition prg in
from_prg := ProgMap.remove prg.prg_name !from_prg;
Defined cst)
else (
let len = Array.length obls in
let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
- from_prg := ProgMap.add n prg !from_prg;
+ from_prg := ProgMap.add n prg !from_prg;
let res = auto_solve_obligations (Some n) tactic in
match res with
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-
+
let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
@@ -576,23 +576,23 @@ let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun
!from_prg l
in
from_prg := upd;
- let _defined =
- List.fold_left (fun finished x ->
- if finished then finished
+ let _defined =
+ List.fold_left (fun finished x ->
+ if finished then finished
else
let res = auto_solve_obligations (Some x) tactic in
match res with
| Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
- | _ -> false)
+ | _ -> false)
false deps
in ()
-
+
let admit_obligations n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
- Array.iteri (fun i x ->
- match x.obl_body with
- None ->
+ Array.iteri (fun i x ->
+ match x.obl_body with
+ None ->
let x = subst_deps_obl obls x in
let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in
assumption_message x.obl_name;
@@ -603,7 +603,7 @@ let admit_obligations n =
exception Found of int
-let array_find f arr =
+let array_find f arr =
try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
raise Not_found
with Found i -> i
@@ -611,9 +611,9 @@ let array_find f arr =
let next_obligation n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
- let i =
+ let i =
try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
with Not_found -> anomaly "Could not find a solvable obligation."
in solve_obligation prg i
-
+
let default_tactic () = !default_tactic
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 2afcb19413..80d5b9465c 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -4,8 +4,8 @@ open Libnames
open Evd
open Proof_type
-type obligation_info =
- (identifier * Term.types * loc *
+type obligation_info =
+ (identifier * Term.types * loc *
obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array
(* ident, type, location, (opaque or transparent, expand or define),
dependencies, tactic to solve it *)
@@ -14,14 +14,14 @@ type progress = (* Resolution status of a program *)
| Remain of int (* n obligations remaining *)
| Dependent (* Dependent on other definitions *)
| Defined of global_reference (* Defined as id *)
-
+
val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
val default_tactic : unit -> Proof_type.tactic
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
val get_proofs_transparency : unit -> bool
-val add_definition : Names.identifier -> Term.constr -> Term.types ->
+val add_definition : Names.identifier -> Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
@@ -29,9 +29,9 @@ val add_definition : Names.identifier -> Term.constr -> Term.types ->
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
-val add_mutual_definitions :
+val add_mutual_definitions :
(Names.identifier * Term.constr * Term.types *
- (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+ (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
?tactic:Proof_type.tactic ->
?kind:Decl_kinds.definition_kind ->
?hook:Tacexpr.declaration_hook ->
@@ -45,7 +45,7 @@ val next_obligation : Names.identifier option -> unit
val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
(* Number of remaining obligations to be solved for this program *)
-val solve_all_obligations : Proof_type.tactic option -> unit
+val solve_all_obligations : Proof_type.tactic option -> unit
val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 91418e05e7..e705e73c16 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -23,7 +23,7 @@ open Typeops
open Libnames
open Classops
open List
-open Recordops
+open Recordops
open Evarutil
open Pretype_errors
open Rawterm
@@ -54,7 +54,7 @@ type recursion_info = {
f_fulltype: types; (* Type with argument and wf proof product first *)
}
-let my_print_rec_info env t =
+let my_print_rec_info env t =
str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
@@ -65,10 +65,10 @@ let my_print_rec_info env t =
(* str " and tycon "++ my_print_tycon env tycon ++ *)
(* str " in environment: " ++ my_print_env env); *)
-let merge_evms x y =
+let merge_evms x y =
Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y
-let interp env isevars c tycon =
+let interp env isevars c tycon =
let j = pretype tycon env isevars ([],[]) c in
let _ = isevars := Evarutil.nf_evar_defs !isevars in
let evd,_ = consider_remaining_unif_problems env !isevars in
@@ -92,7 +92,7 @@ let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constr
let env_with_binders env isevars l =
let rec aux ((env, rels) as acc) = function
- Topconstr.LocalRawDef ((loc, name), def) :: tl ->
+ Topconstr.LocalRawDef ((loc, name), def) :: tl ->
let rawdef = coqintern_constr !isevars env def in
let coqdef, deftyp = interp env isevars rawdef empty_tycon in
let reldecl = (name, Some coqdef, deftyp) in
@@ -100,10 +100,10 @@ let env_with_binders env isevars l =
| Topconstr.LocalRawAssum (bl, k, typ) :: tl ->
let rawtyp = coqintern_type !isevars env typ in
let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
- let acc =
- List.fold_left (fun (env, rels) (loc, name) ->
+ let acc =
+ List.fold_left (fun (env, rels) (loc, name) ->
let reldecl = (name, None, coqtyp) in
- (push_rel reldecl env,
+ (push_rel reldecl env,
reldecl :: rels))
(env, rels) bl
in aux acc tl
@@ -112,15 +112,15 @@ let env_with_binders env isevars l =
let subtac_process env isevars id bl c tycon =
let c = Command.abstract_constr_expr c bl in
- let tycon =
+ let tycon =
match tycon with
None -> empty_tycon
- | Some t ->
+ | Some t ->
let t = Command.generalize_constr_expr t bl in
let t = coqintern_type !isevars env t in
let coqt, ttyp = interp env isevars t empty_tycon in
mk_tycon coqt
- in
+ in
let c = coqintern_constr !isevars env c in
let imps = Implicit_quantifiers.implicits_of_rawterm c in
let coqc, ctyp = interp env isevars c tycon in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index a1d9603187..f818379e73 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -24,7 +24,7 @@ open Libnames
open Nameops
open Classops
open List
-open Recordops
+open Recordops
open Evarutil
open Pretype_errors
open Rawterm
@@ -65,27 +65,27 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let (evd',t) = f !evdref x y z in
evdref := evd';
t
-
+
let mt_evd = Evd.empty
-
+
(* Utilisé pour inférer le prédicat des Cases *)
(* Semble exagérement fort *)
(* Faudra préférer une unification entre les types de toutes les clauses *)
(* et autoriser des ? à rester dans le résultat de l'unification *)
-
+
let evar_type_fixpoint loc env evdref lna lar vdefj =
- let lt = Array.length vdefj in
- if Array.length lar = lt then
- for i = 0 to lt-1 do
+ let lt = Array.length vdefj in
+ if Array.length lar = lt then
+ for i = 0 to lt-1 do
if not (e_cumul env evdref (vdefj.(i)).uj_type
(lift lt lar.(i))) then
error_ill_typed_rec_body_loc loc env ( !evdref)
i lna vdefj lar
done
- let check_branches_message loc env evdref c (explft,lft) =
+ let check_branches_message loc env evdref c (explft,lft) =
for i = 0 to Array.length explft - 1 do
- if not (e_cumul env evdref lft.(i) explft.(i)) then
+ if not (e_cumul env evdref lft.(i) explft.(i)) then
let sigma = !evdref in
error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
done
@@ -137,19 +137,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
if n=0 then p else
match kind_of_term p with
| Lambda (_,_,c) -> decomp (n-1) c
- | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
+ | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
in
let sign,s = decompose_prod_n n pj.uj_type in
let ind = build_dependent_inductive env indf in
let s' = mkProd (Anonymous, ind, s) in
let ccl = lift 1 (decomp n pj.uj_val) in
let ccl' = mkLambda (Anonymous, ind, ccl) in
- {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
+ {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
(*************************************************************************)
(* Main pretyping function *)
- let pretype_ref evdref env ref =
+ let pretype_ref evdref env ref =
let c = constr_of_global ref in
make_judge c (Retyping.get_type_of env Evd.empty c)
@@ -160,7 +160,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [( evdref)] and *)
(* the type constraint tycon *)
- let rec pretype (tycon : type_constraint) env evdref lvar c =
+ let rec pretype (tycon : type_constraint) env evdref lvar c =
(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *)
(* with _ -> () *)
@@ -187,12 +187,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let j = (Retyping.get_judgment_of env ( !evdref) c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
- | RPatVar (loc,(someta,n)) ->
+ | RPatVar (loc,(someta,n)) ->
anomaly "Found a pattern variable in a rawterm to type"
-
+
| RHole (loc,k) ->
let ty =
- match tycon with
+ match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
@@ -221,19 +221,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let nbfix = Array.length lar in
let names = Array.map (fun id -> Name id) names in
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
- let newenv =
- let marked_ftys =
+ let newenv =
+ let marked_ftys =
Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in
mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |]))
ftys
in
- push_rec_types (names,marked_ftys,[||]) env
+ push_rec_types (names,marked_ftys,[||]) env
in
let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
let vdefj =
- array_map2_i
+ array_map2_i
(fun i ctxt def ->
- let fty =
+ let fty =
let ty = ftys.(i) in
if i = fixi then (
Option.iter (fun tycon ->
@@ -260,19 +260,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* First, let's find the guard indexes. *)
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
- but doing it properly involves delta-reduction, and it finally
- doesn't seem worth the effort (except for huge mutual
+ but doing it properly involves delta-reduction, and it finally
+ doesn't seem worth the effort (except for huge mutual
fixpoints ?) *)
- let possible_indexes = Array.to_list (Array.mapi
- (fun i (n,_) -> match n with
+ let possible_indexes = Array.to_list (Array.mapi
+ (fun i (n,_) -> match n with
| Some n -> [n]
| None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
vn)
- in
- let fixdecls = (names,ftys,fdefs) in
- let indexes = search_guard loc env possible_indexes fixdecls in
+ in
+ let fixdecls = (names,ftys,fdefs) in
+ let indexes = search_guard loc env possible_indexes fixdecls in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
- | RCoFix i ->
+ | RCoFix i ->
let cofix = (i,(names,ftys,fdefs)) in
(try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
make_judge (mkCoFix cofix) ftys.(i) in
@@ -281,10 +281,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RSort (loc,s) ->
inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
- | RApp (loc,f,args) ->
- let length = List.length args in
+ | RApp (loc,f,args) ->
+ let length = List.length args in
let ftycon =
- let ty =
+ let ty =
if length > 0 then
match tycon with
| None -> None
@@ -292,7 +292,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| Some (Some (init, cur), ty) ->
Some (Some (length + init, length + cur), ty)
else tycon
- in
+ in
match ty with
| Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
| _ -> None
@@ -314,14 +314,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
let typ' = nf_evar !evdref typ in
- apply_rec env (n+1)
+ apply_rec env (n+1)
{ uj_val = nf_evar !evdref value;
uj_type = nf_evar !evdref typ' }
(Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
- error_cant_apply_not_functional_loc
+ error_cant_apply_not_functional_loc
(join_loc floc argloc) env ( !evdref)
resj [hj]
in
@@ -337,20 +337,20 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref resj tycon
| RLambda(loc,name,k,c1,c2) ->
- let tycon' = evd_comb1
- (fun evd tycon ->
- match tycon with
- | None -> evd, tycon
- | Some ty ->
+ let tycon' = evd_comb1
+ (fun evd tycon ->
+ match tycon with
+ | None -> evd, tycon
+ | Some ty ->
let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in
- evd, Some ty')
- evdref tycon
+ evd, Some ty')
+ evdref tycon
in
let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in
let dom_valcon = valcon_of_tycon dom in
let j = pretype_type dom_valcon env evdref lvar c1 in
let var = (name,None,j.utj_val) in
- let j' = pretype rng (push_rel var env) evdref lvar c2 in
+ let j' = pretype rng (push_rel var env) evdref lvar c2 in
let resj = judge_of_abstraction env name j j' in
inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -363,7 +363,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
try judge_of_product env name j j'
with TypeError _ as e -> Stdpp.raise_with_loc loc e in
inh_conv_coerce_to_tycon loc env evdref resj tycon
-
+
| RLetIn(loc,name,c1,c2) ->
let j = pretype empty_tycon env evdref lvar c1 in
let t = refresh_universes j.uj_type in
@@ -375,11 +375,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env evdref lvar c in
- let (IndType (indf,realargs)) =
+ let (IndType (indf,realargs)) =
try find_rectype env ( !evdref) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env ( !evdref) cj
+ error_case_not_inductive_loc cloc env ( !evdref) cj
in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 1 then
@@ -406,7 +406,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let ccl = nf_evar ( !evdref) pj.utj_val in
let psign = make_arity_signature env true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
- let inst =
+ let inst =
(Array.to_list cs.cs_concl_realargs)
@[build_dependent_constructor cs] in
let lp = lift cs.cs_nargs p in
@@ -416,45 +416,45 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let v =
let mis,_ = dest_ind_family indf in
let ci = make_case_info env mis LetStyle in
- mkCase (ci, p, cj.uj_val,[|f|]) in
+ mkCase (ci, p, cj.uj_val,[|f|]) in
{ uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
- | None ->
+ | None ->
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f evdref lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let ccl = nf_evar ( !evdref) fj.uj_type in
let ccl =
if noccur_between 1 cs.cs_nargs ccl then
- lift (- cs.cs_nargs) ccl
+ lift (- cs.cs_nargs) ccl
else
- error_cant_find_case_type_loc loc env ( !evdref)
+ error_cant_find_case_type_loc loc env ( !evdref)
cj.uj_val in
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
let mis,_ = dest_ind_family indf in
let ci = make_case_info env mis LetStyle in
- mkCase (ci, p, cj.uj_val,[|f|] )
+ mkCase (ci, p, cj.uj_val,[|f|] )
in
{ uj_val = v; uj_type = ccl })
| RIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
- let (IndType (indf,realargs)) =
+ let (IndType (indf,realargs)) =
try find_rectype env ( !evdref) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
error_case_not_inductive_loc cloc env ( !evdref) cj in
- let cstrs = get_constructors env indf in
+ let cstrs = get_constructors env indf in
if Array.length cstrs <> 2 then
user_err_loc (loc,"",
str "If is only for inductive types with two constructors.");
- let arsgn =
+ let arsgn =
let arsgn,_ = get_arity env indf in
if not !allow_anonymous_refs then
(* Make dependencies from arity signature impossible *)
- List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
else arsgn
in
let nar = List.length arsgn in
@@ -467,10 +467,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let pred = it_mkLambda_or_LetIn ccl psign in
let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
- uj_type = typ} tycon
+ uj_type = typ} tycon
in
jtyp.uj_val, jtyp.uj_type
- | None ->
+ | None ->
let p = match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
@@ -484,18 +484,18 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let n = rel_context_length cs.cs_args in
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist (pi, [build_dependent_constructor cs]) in
- let csgn =
+ let csgn =
if not !allow_anonymous_refs then
- List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
- else
- List.map
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
+ else
+ List.map
(fun (n, b, t) ->
match n with
Name _ -> (n, b, t)
| Anonymous -> (Name (id_of_string "H"), b, t))
cs.cs_args
in
- let env_c = push_rels csgn env in
+ let env_c = push_rels csgn env in
(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
let bj = pretype (mk_tycon pi) env_c evdref lvar b in
it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
@@ -548,7 +548,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let t = Retyping.get_type_of env sigma v in
match kind_of_term (whd_betadeltaiota env sigma t) with
| Sort s -> s
- | Evar ev when is_Type (existential_type sigma ev) ->
+ | Evar ev when is_Type (existential_type sigma ev) ->
evd_comb1 (define_evar_as_sort) evdref ev
| _ -> anomaly "Found a type constraint which is not a type"
in
@@ -579,7 +579,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(pretype_type empty_valcon env evdref lvar c).utj_val in
evdref := fst (consider_remaining_unif_problems env !evdref);
if resolve_classes then
- evdref :=
+ evdref :=
Typeclasses.resolve_typeclasses ~onlyargs:false
~split:true ~fail:fail_evar env !evdref;
let c = nf_evar !evdref c' in
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 645e3e23ec..288d3854fd 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -40,7 +40,7 @@ let sig_ref = make_ref "Init.Specif.sig"
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
-let build_sig () =
+let build_sig () =
{ proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
elim = init_constant ["Init"; "Specif"] "sig_rec";
@@ -67,13 +67,13 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
-let jmeq_ind =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
+let jmeq_ind =
+ lazy (check_required_library ["Coq";"Logic";"JMeq"];
init_constant ["Logic";"JMeq"] "JMeq")
-let jmeq_rec =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
+let jmeq_rec =
+ lazy (check_required_library ["Coq";"Logic";"JMeq"];
init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_refl =
+let jmeq_refl =
lazy (check_required_library ["Coq";"Logic";"JMeq"];
init_constant ["Logic";"JMeq"] "JMeq_refl")
@@ -88,7 +88,7 @@ let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
-
+
let existS = lazy (build_sigma_type ())
let prod = lazy (build_prod ())
@@ -120,20 +120,20 @@ let debug_level = 2
let debug_on = true
-let debug n s =
+let debug n s =
if debug_on then
if !Flags.debug && n >= debug_level then
msgnl s
else ()
else ()
-let debug_msg n s =
+let debug_msg n s =
if debug_on then
if !Flags.debug && n >= debug_level then s
else mt ()
else mt ()
-let trace s =
+let trace s =
if debug_on then
if !Flags.debug && debug_level > 0 then msgnl s
else ()
@@ -145,28 +145,28 @@ let rec pp_list f = function
let wf_relations = Hashtbl.create 10
-let std_relations () =
+let std_relations () =
let add k v = Hashtbl.add wf_relations k v in
add (init_constant ["Init"; "Peano"] "lt")
(lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
-
+
let std_relations = Lazy.lazy_from_fun std_relations
type binders = Topconstr.local_binder list
-let app_opt c e =
+let app_opt c e =
match c with
Some constr -> constr e
- | None -> e
+ | None -> e
-let print_args env args =
+let print_args env args =
Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
let make_existential loc ?(opaque = Define true) env isevars c =
let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
let (key, args) = destEvar evar in
(try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
- print_args env args ++ str " for type: "++
+ print_args env args ++ str " for type: "++
my_print_constr env c) with _ -> ());
evar
@@ -186,29 +186,29 @@ let string_of_hole_kind = function
| GoalEvar -> "GoalEvar"
| ImpossibleCase -> "ImpossibleCase"
-let evars_of_term evc init c =
+let evars_of_term evc init c =
let rec evrec acc c =
match kind_of_term c with
| Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
| Evar (n, _) -> assert(false)
| _ -> fold_constr evrec acc c
- in
+ in
evrec init c
let non_instanciated_map env evd evm =
- List.fold_left
- (fun evm (key, evi) ->
+ List.fold_left
+ (fun evm (key, evi) ->
let (loc,k) = evar_source key !evd in
- debug 2 (str "evar " ++ int key ++ str " has kind " ++
+ debug 2 (str "evar " ++ int key ++ str " has kind " ++
str (string_of_hole_kind k));
- match k with
+ match k with
| QuestionMark _ -> Evd.add evm key evi
| ImplicitArg (_,_,false) -> Evd.add evm key evi
| _ ->
debug 2 (str " and is an implicit");
Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
Evd.empty (Evarutil.non_instantiated evm)
-
+
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
@@ -222,7 +222,7 @@ open Tactics
open Tacticals
let id x = x
-let filter_map f l =
+let filter_map f l =
let rec aux acc = function
hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
| None -> aux acc tl)
@@ -237,36 +237,36 @@ let build_dependent_sum l =
(try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
with _ -> ());
let tac = assert_tac (Name n) hyptype in
- let conttac =
- (fun cont ->
+ let conttac =
+ (fun cont ->
conttac
(tclTHENS tac
([intros;
- (tclTHENSEQ
- [constructor_tac false (Some 1) 1
+ (tclTHENSEQ
+ [constructor_tac false (Some 1) 1
(Rawterm.ImplicitBindings [inj_open (mkVar n)]);
cont]);
])))
in
- let conttype =
- (fun typ ->
+ let conttype =
+ (fun typ ->
let tex = mkLambda (Name n, t, typ) in
conttype
(mkApp (Lazy.force ex_ind, [| t; tex |])))
in
aux (mkVar n :: names) conttac conttype tl
- | (n, t) :: [] ->
+ | (n, t) :: [] ->
(conttac intros, conttype t)
| [] -> raise (Invalid_argument "build_dependent_sum")
- in aux [] id id (List.rev l)
-
+ in aux [] id id (List.rev l)
+
open Proof_type
open Tacexpr
-let mkProj1 a b c =
+let mkProj1 a b c =
mkApp (Lazy.force proj1, [| a; b; c |])
-let mkProj2 a b c =
+let mkProj2 a b c =
mkApp (Lazy.force proj2, [| a; b; c |])
let mk_ex_pi1 a b c =
@@ -274,8 +274,8 @@ let mk_ex_pi1 a b c =
let mk_ex_pi2 a b c =
mkApp (Lazy.force ex_pi2, [| a; b; c |])
-
-let mkSubset name typ prop =
+
+let mkSubset name typ prop =
mkApp ((Lazy.force sig_).typ,
[| typ; mkLambda (name, typ, prop) |])
@@ -300,22 +300,22 @@ let mk_not c =
mkApp (notc, [| c |])
let and_tac l hook =
- let andc = Coqlib.build_coq_and () in
+ let andc = Coqlib.build_coq_and () in
let rec aux ((accid, goal, tac, extract) as acc) = function
| [] -> (* Singleton *) acc
-
+
| (id, x, elgoal, eltac) :: tl ->
let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
let proj = fun c -> mkProj2 goal elgoal c in
let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
- aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
+ aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
(id, x, elgoal, proj) :: extract) tl
in
- let and_proof_id, and_goal, and_tac, and_extract =
+ let and_proof_id, and_goal, and_tac, and_extract =
match l with
| [] -> raise (Invalid_argument "and_tac: empty list of goals")
- | (hdid, x, hdg, hdt) :: tl ->
+ | (hdid, x, hdg, hdt) :: tl ->
aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
in
let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
@@ -324,20 +324,20 @@ let and_tac l hook =
trace (str "Started and proof");
Pfedit.by and_tac;
trace (str "Applied and tac")
-
-let destruct_ex ext ex =
- let rec aux c acc =
+
+let destruct_ex ext ex =
+ let rec aux c acc =
match kind_of_term c with
App (f, args) ->
(match kind_of_term f with
Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
- let (dom, rng) =
+ let (dom, rng) =
try (args.(0), args.(1))
with _ -> assert(false)
in
let pi1 = (mk_ex_pi1 dom rng acc) in
- let rng_body =
+ let rng_body =
match kind_of_term rng with
Lambda (_, _, t) -> subst1 pi1 t
| t -> rng
@@ -348,14 +348,14 @@ let destruct_ex ext ex =
in aux ex ext
open Rawterm
-
+
let id_of_name = function
Name n -> n
| Anonymous -> raise (Invalid_argument "id_of_name")
let definition_message id =
Nameops.pr_id id ++ str " is defined"
-
+
let recursive_message v =
match Array.length v with
| 0 -> error "no recursive definition"
@@ -398,7 +398,7 @@ let rec string_of_list sep f = function
| x :: [] -> f x
| x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
-let string_of_intset d =
+let string_of_intset d =
string_of_list "," string_of_int (Intset.elements d)
(**********************************************************)
@@ -416,20 +416,20 @@ let pr_meta_map evd =
| _ -> mt() in
let pr_meta_binding = function
| (mv,Cltyp (na,b)) ->
- hov 0
+ hov 0
(pr_meta mv ++ pr_name na ++ str " : " ++
print_constr b.rebus ++ fnl ())
| (mv,Clval(na,b,_)) ->
- hov 0
+ hov 0
(pr_meta mv ++ pr_name na ++ str " := " ++
print_constr (fst b).rebus ++ fnl ())
in
- prlist pr_meta_binding ml
+ prlist pr_meta_binding ml
let pr_idl idl = prlist_with_sep pr_spc pr_id idl
let pr_evar_info evi =
- let phyps =
+ let phyps =
(*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
Printer.pr_named_context (Global.env()) (evar_context evi)
in
@@ -442,7 +442,7 @@ let pr_evar_info evi =
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
let pr_evar_defs sigma =
- h 0
+ h 0
(prlist_with_sep pr_fnl
(fun (ev,evi) ->
h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
@@ -454,7 +454,7 @@ let pr_constraints pbs =
print_constr t1 ++ spc() ++
str (match pbty with
| Reduction.CONV -> "=="
- | Reduction.CUMUL -> "<=") ++
+ | Reduction.CUMUL -> "<=") ++
spc() ++ print_constr t2) pbs)
let pr_evar_defs evd =
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index dff1df8f96..e7ee6c7483 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -85,7 +85,7 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t
type binders = local_binder list
val app_opt : ('a -> 'a) option -> 'a -> 'a
val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> ?opaque:obligation_definition_status ->
+val make_existential : loc -> ?opaque:obligation_definition_status ->
env -> evar_defs ref -> types -> constr
val make_existential_expr : loc -> 'a -> 'b -> constr_expr
val string_of_hole_kind : hole_kind -> string
@@ -111,7 +111,7 @@ val mk_conj : types list -> types
val mk_not : types -> types
val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
-val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
+val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
val destruct_ex : constr -> constr -> constr list
diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
index da612c4367..e3dbd127f9 100644
--- a/plugins/subtac/test/ListDep.v
+++ b/plugins/subtac/test/ListDep.v
@@ -22,7 +22,7 @@ Section Map_DependentRecursor.
Variable l : list U.
Variable f : { x : U | In x l } -> V.
- Obligations Tactic := unfold sub_list in * ;
+ Obligations Tactic := unfold sub_list in * ;
program_simpl ; intuition.
Program Fixpoint map_rec ( l' : list U | sub_list l' l )
@@ -32,16 +32,16 @@ Section Map_DependentRecursor.
| cons x tl => let tl' := map_rec tl in
f x :: tl'
end.
-
+
Next Obligation.
destruct_call map_rec.
simpl in *.
subst l'.
simpl ; auto with arith.
Qed.
-
+
Program Definition map : list V := map_rec l.
-
+
End Map_DependentRecursor.
Extraction map.
diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
index 05fc0803fc..2cea0841de 100644
--- a/plugins/subtac/test/ListsTest.v
+++ b/plugins/subtac/test/ListsTest.v
@@ -7,7 +7,7 @@ Set Implicit Arguments.
Section Accessors.
Variable A : Set.
- Program Definition myhd : forall (l : list A | length l <> 0), A :=
+ Program Definition myhd : forall (l : list A | length l <> 0), A :=
fun l =>
match l with
| nil => !
@@ -34,22 +34,22 @@ Section app.
match l with
| nil => l'
| hd :: tl => hd :: (tl ++ l')
- end
+ end
where "x ++ y" := (app x y).
Next Obligation.
intros.
destruct_call app ; program_simpl.
Defined.
-
+
Program Lemma app_id_l : forall l : list A, l = nil ++ l.
Proof.
simpl ; auto.
Qed.
-
+
Program Lemma app_id_r : forall l : list A, l = l ++ nil.
Proof.
- induction l ; simpl in * ; auto.
+ induction l ; simpl in * ; auto.
rewrite <- IHl ; auto.
Qed.
@@ -61,7 +61,7 @@ Section Nth.
Variable A : Set.
- Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
+ Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
match n, l with
| 0, hd :: _ => hd
| S n', _ :: tl => nth tl n'
@@ -70,7 +70,7 @@ Section Nth.
Next Obligation.
Proof.
- simpl in *. auto with arith.
+ simpl in *. auto with arith.
Defined.
Next Obligation.
@@ -78,7 +78,7 @@ Section Nth.
inversion H.
Qed.
- Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
+ Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
match l, n with
| hd :: _, 0 => hd
| _ :: tl, S n' => nth' tl n'
@@ -86,7 +86,7 @@ Section Nth.
end.
Next Obligation.
Proof.
- simpl in *. auto with arith.
+ simpl in *. auto with arith.
Defined.
Next Obligation.
diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
index ac49ca96a4..01e2d75f33 100644
--- a/plugins/subtac/test/Mutind.v
+++ b/plugins/subtac/test/Mutind.v
@@ -1,11 +1,11 @@
Require Import List.
-Program Fixpoint f a : { x : nat | x > 0 } :=
+Program Fixpoint f a : { x : nat | x > 0 } :=
match a with
| 0 => 1
| S a' => g a a'
end
-with g a b : { x : nat | x > 0 } :=
+with g a b : { x : nat | x > 0 } :=
match b with
| 0 => 1
| S b' => f b'
diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
index 14b8085496..7e0755d571 100644
--- a/plugins/subtac/test/Test1.v
+++ b/plugins/subtac/test/Test1.v
@@ -1,4 +1,4 @@
-Program Definition test (a b : nat) : { x : nat | x = a + b } :=
+Program Definition test (a b : nat) : { x : nat | x = a + b } :=
((a + b) : { x : nat | x = a + b }).
Proof.
intros.
diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
index 501aa79815..97c3d9414d 100644
--- a/plugins/subtac/test/euclid.v
+++ b/plugins/subtac/test/euclid.v
@@ -1,12 +1,12 @@
Require Import Coq.Program.Program.
Require Import Coq.Arith.Compare_dec.
Notation "( x & y )" := (existS _ x y) : core_scope.
-
+
Require Import Omega.
Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} :
{ q : nat & { r : nat | a = b * q + r /\ r < b } } :=
- if le_lt_dec b a then let (q', r) := euclid (a - b) b in
+ if le_lt_dec b a then let (q', r) := euclid (a - b) b in
(S q' & r)
else (O & a).
diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v
index 2e17959c3e..90ae8bae84 100644
--- a/plugins/subtac/test/take.v
+++ b/plugins/subtac/test/take.v
@@ -11,7 +11,7 @@ Print cons.
Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
match n with
| 0 => nil
- | S p =>
+ | S p =>
match l with
| cons hd tl => let rest := take tl p in cons hd rest
| nil => !
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v
index 49fec2b80c..5ccc154afd 100644
--- a/plugins/subtac/test/wf.v
+++ b/plugins/subtac/test/wf.v
@@ -29,7 +29,7 @@ Require Import Wf_nat.
Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} :
{ q : nat & { r : nat | a = b * q + r /\ r < b } } :=
- if le_lt_dec b a then let (q', r) := euclid (a - b) b in
+ if le_lt_dec b a then let (q', r) := euclid (a - b) b in
(S q' & r)
else (O & a).
destruct b ; simpl_subtac.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 16:07:44 +0000