aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-27 10:52:47 +0200
committerPierre-Marie Pédrot2016-09-27 10:52:47 +0200
commit8042a9078cb8ee8736593356d1a09311c8eeff2f (patch)
tree85274f5a4327beb960f0bbbac5c710ba3d7b8506
parent160a6d8806516b40d6406ebe0ae6c0240e969d85 (diff)
parente6a054695a2f5d8be3f695975464f99571a69b75 (diff)
Merge branch 'v8.5' into v8.6
-rw-r--r--tactics/tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ce77df69f4..2d901c2dbc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -377,7 +377,7 @@ let rename_hyp repl =
let nctx = Environ.val_of_named_context nhyps in
let instance = List.map (mkVar % get_id) hyps in
Refine.refine ~unsafe:true { run = begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~store instance
+ Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
end }
end }