diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 441fb68acc..c030c77d4d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -70,19 +70,19 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) let connect_hint_clenv poly (c, _, ctx) clenv gl = - (** [clenv] has been generated by a hint-making function, so the only relevant - data in its evarmap is the set of metas. The [evar_reset_evd] function - below just replaces the metas of sigma by those coming from the clenv. *) + (* [clenv] has been generated by a hint-making function, so the only relevant + data in its evarmap is the set of metas. The [evar_reset_evd] function + below just replaces the metas of sigma by those coming from the clenv. *) let sigma = Tacmach.New.project gl in let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in - (** Still, we need to update the universes *) + (* Still, we need to update the universes *) let clenv, c = if poly then - (** Refresh the instance of the hint *) + (* Refresh the instance of the hint *) let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - (** Only metas are mentioning the old universes. *) + (* Only metas are mentioning the old universes. *) let clenv = { templval = Evd.map_fl emap clenv.templval; templtyp = Evd.map_fl emap clenv.templtyp; |