diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 848b44a603..ea985ddecd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -66,9 +66,9 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b + match rt.CAst.v with + | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -80,8 +80,8 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + match rt.CAst.v with + | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -103,7 +103,7 @@ let list_add_set_eq eq_fun x l = let const_of_id id = let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.ghost,id)) + qualid_of_reference (Libnames.Ident (Loc.tag id)) in try Constrintern.locate_reference princ_ref with Not_found -> @@ -422,7 +422,6 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { - optsync = false; optdepr = false; optname = "Functional Induction Rewrite Dependent"; optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; @@ -435,7 +434,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t let function_debug_sig = { - optsync = false; optdepr = false; optname = "Function debug"; optkey = ["Function_debug"]; @@ -454,7 +452,6 @@ let strict_tcc = ref false let is_strict_tcc () = !strict_tcc let strict_tcc_sig = { - optsync = false; optdepr = false; optname = "Raw Function Tcc"; optkey = ["Function_raw_tcc"]; |