diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /pretyping/cases.ml | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fe67f5767b..62c27297f3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1015,9 +1015,9 @@ let add_assert_false_case pb tomatch = let adjust_impossible_cases sigma pb pred tomatch submat = match submat with | [] -> - (** FIXME: This breaks if using evar-insensitive primitives. In particular, - this means that the Evd.define below may redefine an already defined - evar. See e.g. first definition of test for bug #3388. *) + (* FIXME: This breaks if using evar-insensitive primitives. In particular, + this means that the Evd.define below may redefine an already defined + evar. See e.g. first definition of test for bug #3388. *) let pred = EConstr.Unsafe.to_constr pred in begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk sigma) == Evar_kinds.ImpossibleCase -> @@ -1684,8 +1684,8 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = convertible subterms of the substitution *) let evdref = ref sigma in let rec aux (k,env,subst as x) t = - (** Use a reference because the [map_constr_with_full_binders] does not - allow threading a state. *) + (* Use a reference because the [map_constr_with_full_binders] does not + allow threading a state. *) let sigma = !evdref in match EConstr.kind sigma t with | Rel n when is_local_def (lookup_rel n !!env) -> t @@ -2021,7 +2021,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let refresh_tycon sigma t = - (** If we put the typing constraint in the term, it has to be + (* If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe can appear in the term. *) refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) |