diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 30 |
1 files changed, 17 insertions, 13 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da30bd9c9..34283c49c3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -2,6 +2,7 @@ open Printer open CErrors open Util open Constr +open Context open EConstr open Vars open Namegen @@ -238,7 +239,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; @@ -300,7 +303,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let old_context_length = List.length context + 1 in let witness_fun = - mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t, + mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t, mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) ) in @@ -310,7 +313,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) + (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl, + witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -426,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = else if isProd sigma type_of_hyp then begin - let (x,t_x,t') = destProd sigma type_of_hyp in + let (x,t_x,t') = destProd sigma type_of_hyp in let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in if is_property sigma ptes_infos t_x actual_real_type_of_hyp then begin @@ -539,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with NoChange -> (* Last thing todo : push the rel in the context and continue *) - scan_type (LocalAssum (x,t_x) :: context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -608,7 +612,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = anomaly (Pp.str "cannot compute new term value.") in let fun_body = - mkLambda(Anonymous, + mkLambda(make_annot Anonymous Sorts.Relevant, pf_unsafe_type_of g' term, Termops.replace_term (project g') term (mkRel 1) dyn_infos.info ) @@ -734,7 +738,7 @@ let build_proof g in build_proof do_finalize_t {dyn_infos with info = t} g - | Lambda(n,t,b) -> + | Lambda(n,t,b) -> begin match EConstr.kind sigma (pf_concl g) with | Prod _ -> @@ -1147,7 +1151,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let fix_offset = List.length princ_params in let ptes_to_fix,infos = match EConstr.kind (project g) fbody_with_full_params with - | Fix((idxs,i),(names,typess,bodies)) -> + | Fix((idxs,i),(names,typess,bodies)) -> let bodies_with_all_params = Array.map (fun body -> @@ -1162,7 +1166,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (fun i types -> let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; - name = Nameops.Name.get_id (fresh_id names.(i)); + name = Nameops.Name.get_id (fresh_id names.(i).binder_name); types = types; offset = fix_offset; nb_realargs = @@ -1193,9 +1197,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with - | Fix((_,num),(_,_,bs)) -> + | Fix((_,num),(_,_,bs)) -> Reductionops.nf_betaiota (pf_env g) (project g) - ( + ( (applist (substl (List.rev @@ -1512,7 +1516,7 @@ let is_valid_hypothesis sigma predicates_name = let rec is_valid_hypothesis typ = is_pte typ || match EConstr.kind sigma typ with - | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' + | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' | _ -> false in is_valid_hypothesis @@ -1563,7 +1567,7 @@ let prove_principle_for_gen in let rec_arg_id = match List.rev post_rec_arg with - | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id + | (LocalAssum ({binder_name=Name id},_) | LocalDef ({binder_name=Name id},_,_)) :: _ -> id | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) |