diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 51bbd9058..7519339ca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -169,7 +169,7 @@ let unsafe_intro env store decl b = Refine.refine ~unsafe:true { run = begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in - let inst = List.map (mkVar % NamedDecl.get_id) (named_context env) in + let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in @@ -366,7 +366,7 @@ let rename_hyp repl = let nhyps = List.map map hyps in let nconcl = subst concl in let nctx = Environ.val_of_named_context nhyps in - let instance = List.map (mkVar % NamedDecl.get_id) hyps in + let instance = List.map (NamedDecl.get_id %> mkVar) hyps in Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~store instance end } |