diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 75b665aad9..fd791a9101 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -664,7 +664,7 @@ type rewrite_result = type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *) env : Environ.env ; - unfresh : Id.t list ; (* Unfresh names *) + unfresh : Id.Set.t; (* Unfresh names *) term1 : constr ; ty1 : types ; (* first term and its type (convertible to rew_from) *) cstr : (bool (* prop *) * constr option) ; @@ -1614,7 +1614,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in try let res = - cl_rewrite_clause_aux ?abs strat env [] sigma ty clause + cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context sigma in + let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = |