Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Logic variables in clauses are represented as capital constants.

It is a Prolog convention to give capitalized names to logicl variables
and lower cased names to real constants
  • Loading branch information...
commit af63633091498b7620d8faddbc4d476b375a40bd 1 parent 018867a
@yvting authored
Showing with 1 addition and 1 deletion.
  1. +1 −1  src/tactics.ml
View
2  src/tactics.ml
@@ -31,7 +31,7 @@ let rec replace_pi_with_const term ~used =
match tc [] abs with
| Ty(ty::_, _) ->
let (c, used') =
- fresh_wrt ~ts:0 Constant (prefix Constant) ty used in
+ fresh_wrt ~ts:0 Constant "X" ty used in
replace_pi_with_const (app abs [c]) ~used:used'
| _ -> assert false
else
Please sign in to comment.
Something went wrong with that request. Please try again.