new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
;;
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
+let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
TermUtil.saturate_term newmeta' metasenv' context termty
goal_arity in
let subst,newmetasenv',_ =
- CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+ CicUnification.fo_unif_subst
+ subst context newmetasenv consthead ty CicUniv.empty_ugraph
in
let t =
if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
let subst,newmetasenv',t =
let rec add_one_argument n =
try
- new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
+ new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty
termty n
with CicUnification.UnificationFailure _ when n > 0 ->
add_one_argument (n - 1)
ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
newmetasenv''
in
- let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+ let subst = ((metano,(context,bo',ty))::subst) in
subst,
(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
let n_right_args = List.length right_args in
let n_lambdas = n_right_args + 1 in
let lifted_ty = CicSubstitution.lift n_lambdas ty in
- let replace = ProofEngineReduction.replace_lifting
- ~equality:(CicUtil.alpha_equivalence)
- in
let captured_ty =
let what =
- List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
+ List.map (CicSubstitution.lift n_lambdas) (right_args)
in
- let with_what =
+ let with_what meta =
let rec mkargs = function
- | 0 -> []
- | 1 -> [Cic.Rel 1]
- | n -> (Cic.Rel n)::(mkargs (n-1))
+ | 0 -> assert false
+ | 1 -> []
+ | n ->
+ (if meta then Cic.Implicit None else Cic.Rel n)::(mkargs (n-1))
in
mkargs n_lambdas
in
- replace ~what ~with_what ~where:lifted_ty
+ let replaced = ref false in
+ let replace = ProofEngineReduction.replace_lifting
+ ~equality:(fun _ a b -> let rc = CicUtil.alpha_equivalence a b in
+ if rc then replaced := true; rc)
+ ~context:[]
+ in
+ let captured =
+ replace ~what:[CicSubstitution.lift n_lambdas term]
+ ~with_what:[Cic.Rel 1] ~where:lifted_ty
+ in
+ if not !replaced then
+ (* this means the matched term is not there,
+ * but maybe right params are: we user rels (to right args lambdas) *)
+ replace ~what ~with_what:(with_what false) ~where:captured
+ else
+ (* since the matched is there, rights should be inferrable *)
+ replace ~what ~with_what:(with_what true) ~where:captured
in
let captured_term_ty =
let term_ty = CicSubstitution.lift n_right_args termty in