diff options
| author | Pierre Letouzey | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /pretyping/detyping.ml | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7a1f155bd4..27c1e1e7c5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -180,11 +180,11 @@ let computable p k = A solution could be to store, in the MutCase, the eta-expanded normal form of pred to decide if it depends on its variables - Lorsque le prédicat est dépendant de manière certaine, on - ne déclare pas le prédicat synthétisable (même si la - variable dépendante ne l'est pas effectivement) parce que - sinon on perd la réciprocité de la synthèse (qui, lui, - engendrera un prédicat non dépendant) *) + Lorsque le prédicat est dépendant de manière certaine, on + ne déclare pas le prédicat synthétisable (même si la + variable dépendante ne l'est pas effectivement) parce que + sinon on perd la réciprocité de la synthèse (qui, lui, + engendrera un prédicat non dépendant) *) let sign,ccl = decompose_lam_assum p in Int.equal (rel_context_length sign) (k + 1) @@ -644,7 +644,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran | _, false::l -> (* eta-expansion : n'arrivera plus lorsque tous les - termes seront construits à partir de la syntaxe Cases *) + termes seront construits à partir de la syntaxe Cases *) (* nommage de la nouvelle variable *) let new_b = applist (lift 1 b, [mkRel 1]) in let pat,new_avoid,new_env,new_ids = |
